Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
Sun, 09 Mar 2014 16:37:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 16:00:45 +0100 |
wenzelm |
tuned message: reveal ambiguity where Syntax_Phases.decode_term fails and thus reduces proper_results beforehand, e.g. term "f(x := y)" in ~~/src/HOL/Hoare/Hoare_Logic.thy;
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 13:29:10 +0100 |
wenzelm |
more basic const report (without completion) for known Const within syntax tree, which usually refers to special syntax (without proper @{const_syntax} markers);
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 19:55:08 +0100 |
wenzelm |
proper position for decode_pos, which is relevant for completion;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 17:37:32 +0100 |
wenzelm |
more decisive commitment to get_free vs. the_const;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 16:24:47 +0100 |
wenzelm |
more compact Markup.markup_report: message body may consist of multiple elements;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 16:12:26 +0100 |
wenzelm |
reject internal term names outright, and complete consts instead;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 14:38:54 +0100 |
wenzelm |
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 13:44:01 +0100 |
wenzelm |
more uniform check_const/read_const;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 12:58:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 11:32:16 +0100 |
wenzelm |
clarified treatment of consts -- prefer value-oriented reports;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 10:53:14 +0100 |
wenzelm |
clarified check of internal names;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 10:12:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 18:26:35 +0100 |
wenzelm |
more markup for inner syntax class/type names (notably for completion);
|
file |
diff |
annotate
|
Sat, 01 Mar 2014 23:17:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
Tue, 18 Feb 2014 16:34:02 +0100 |
wenzelm |
generic markup for embedded languages;
|
file |
diff |
annotate
|
Wed, 15 Jan 2014 22:24:57 +0100 |
wenzelm |
general notion of auxiliary bounds within context;
|
file |
diff |
annotate
|
Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 23:26:09 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
Thu, 27 Jun 2013 11:07:48 +0200 |
wenzelm |
clarified printing of type constraints vs. annotations, notably in goal display with its Type_Annotation.ignore_free_types;
|
file |
diff |
annotate
|
Wed, 29 May 2013 11:06:38 +0200 |
wenzelm |
observe type annotations in print translations as well, notably type_constraint_tr';
|
file |
diff |
annotate
|
Tue, 28 May 2013 23:06:32 +0200 |
wenzelm |
explicit support for type annotations within printed syntax trees;
|
file |
diff |
annotate
|
Tue, 28 May 2013 16:29:11 +0200 |
wenzelm |
more explicit Printer.type_emphasis, depending on show_type_emphasis;
|
file |
diff |
annotate
|
Mon, 27 May 2013 22:00:24 +0200 |
wenzelm |
report markup for ast translations;
|
file |
diff |
annotate
|
Mon, 27 May 2013 18:39:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 27 May 2013 18:24:38 +0200 |
wenzelm |
discontinued obsolete show_all_types;
|
file |
diff |
annotate
|
Mon, 27 May 2013 13:55:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 26 May 2013 22:47:00 +0200 |
wenzelm |
position constraint for bound dummy -- more PIDE markup;
|
file |
diff |
annotate
|
Sun, 26 May 2013 21:53:10 +0200 |
wenzelm |
position constraint for dummy_pattern -- more PIDE markup;
|
file |
diff |
annotate
|
Sun, 26 May 2013 20:42:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
Wed, 03 Oct 2012 16:59:58 +0200 |
wenzelm |
more explicit show_type_constraint, show_sort_constraint;
|
file |
diff |
annotate
|
Wed, 03 Oct 2012 16:01:07 +0200 |
wenzelm |
printed "_ofsort" is subject to show_markup as well;
|
file |
diff |
annotate
|
Wed, 03 Oct 2012 14:58:56 +0200 |
wenzelm |
allow position constraints to coexist with 0 or 1 sort constraints;
|
file |
diff |
annotate
|
Mon, 01 Oct 2012 16:37:22 +0200 |
wenzelm |
report sort assignment of visible type variables;
|
file |
diff |
annotate
|
Sat, 29 Sep 2012 20:13:50 +0200 |
wenzelm |
proper handling of constraints stemming from idtyp_ast_tr';
|
file |
diff |
annotate
|
Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
Sat, 29 Sep 2012 16:51:04 +0200 |
wenzelm |
explicit show_types takes preferenced over show_markup;
|
file |
diff |
annotate
|
Sat, 29 Sep 2012 16:17:46 +0200 |
wenzelm |
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
|
file |
diff |
annotate
|
Sat, 29 Sep 2012 13:43:23 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 14 Sep 2012 18:12:41 +0200 |
wenzelm |
clarified markup names;
|
file |
diff |
annotate
|
Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
Sat, 11 Aug 2012 17:24:21 +0200 |
wenzelm |
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
|
file |
diff |
annotate
|
Fri, 10 Aug 2012 15:57:22 +0200 |
wenzelm |
sneak message into "bad" markup as property -- to be displayed after YXML parsing;
|
file |
diff |
annotate
|
Fri, 10 Aug 2012 10:18:07 +0200 |
wenzelm |
more visible markup of malformed input as "bad";
|
file |
diff |
annotate
|
Sat, 17 Mar 2012 13:06:23 +0100 |
wenzelm |
added Syntax.read_typs;
|
file |
diff |
annotate
|
Fri, 17 Feb 2012 15:42:26 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
Thu, 16 Feb 2012 22:18:28 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
Thu, 05 Jan 2012 20:26:01 +0100 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Fri, 25 Nov 2011 23:04:12 +0100 |
wenzelm |
removed obsolete argument (cf. 954e9d6782ea);
|
file |
diff |
annotate
|
Fri, 11 Nov 2011 14:07:20 +0100 |
wenzelm |
discontinued entity text color, notably historic red for classes;
|
file |
diff |
annotate
|
Fri, 11 Nov 2011 12:52:57 +0100 |
wenzelm |
more scalable Proof_Context.prepare_sorts;
|
file |
diff |
annotate
|
Thu, 10 Nov 2011 23:30:50 +0100 |
wenzelm |
more efficient prepare_sorts -- bypass encoded positions;
|
file |
diff |
annotate
|
Thu, 10 Nov 2011 22:54:15 +0100 |
wenzelm |
suppress irrelevant positions;
|
file |
diff |
annotate
|