| 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
|