| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
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 18:24:38 +0200 |
wenzelm |
discontinued obsolete show_all_types;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 21:48:01 +0200 |
wenzelm |
more system options as context-sensitive config options;
|
file |
diff |
annotate
|
| Sun, 12 May 2013 20:25:45 +0200 |
wenzelm |
some system options as context-sensitive config options;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 20:38:02 +0200 |
wenzelm |
clarified output token markup (see also bc22daeed49e);
|
file |
diff |
annotate
|
| Wed, 03 Oct 2012 16:59:58 +0200 |
wenzelm |
more explicit show_type_constraint, show_sort_constraint;
|
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
|
| Wed, 02 May 2012 16:56:25 +0200 |
wenzelm |
avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 23:47:05 +0200 |
wenzelm |
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 21:11:29 +0200 |
wenzelm |
discontinued Syntax.max_pri, which is not really a symbolic parameter;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 15:48:14 +0200 |
wenzelm |
discontinued special status of structure Printer;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 15:02:11 +0200 |
wenzelm |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 17:52:44 +0200 |
wenzelm |
simplified printer context: uniform externing and static token translations;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 21:55:41 +0200 |
wenzelm |
moved type syntax translations to syn_trans.ML;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 17:00:40 +0200 |
wenzelm |
more abstract print translation;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 12:58:13 +0200 |
wenzelm |
moved unparse material to syntax_phases.ML;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 13:32:20 +0100 |
wenzelm |
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
|
file |
diff |
annotate
|
| Sat, 04 Dec 2010 14:57:04 +0100 |
wenzelm |
added Syntax.pretty_priority;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 21:33:19 +0200 |
wenzelm |
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 23:16:21 +0200 |
wenzelm |
turned show_brackets into proper configuration option;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 23:54:48 +0200 |
wenzelm |
turned eta_contract into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 22:57:21 +0200 |
wenzelm |
turned show_structs into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 17:43:44 +0200 |
wenzelm |
turned show_all_types into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 16:36:33 +0200 |
wenzelm |
treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 16:09:12 +0200 |
wenzelm |
more explicit Config.declare vs. Config.declare_global;
|
file |
diff |
annotate
|