| Tue, 07 Jan 2025 22:07:46 +0100 |
wenzelm |
discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);
|
file |
diff |
annotate
|
| Sat, 07 Dec 2024 15:00:43 +0100 |
wenzelm |
clarified signature and caching;
|
file |
diff |
annotate
|
| Sat, 19 Oct 2024 17:00:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 19 Oct 2024 16:54:34 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 19 Oct 2024 16:27:00 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 20:48:01 +0200 |
wenzelm |
print type constraints for consts with mixfix syntax;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 19:00:51 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 19:00:13 +0200 |
wenzelm |
obsolete (see 137ea3d464be);
|
file |
diff |
annotate
|
| Wed, 16 Oct 2024 22:07:04 +0200 |
wenzelm |
show_consts_markup is enabled by default;
|
file |
diff |
annotate
|
| Wed, 16 Oct 2024 21:41:05 +0200 |
wenzelm |
clarified signature (again, reverting ec1023a5c54c);
|
file |
diff |
annotate
|
| Wed, 16 Oct 2024 21:22:37 +0200 |
wenzelm |
clarified signature: more explicit Syntax.print_mode_tabs, depending on print_mode_value ();
|
file |
diff |
annotate
|
| Wed, 16 Oct 2024 19:44:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2024 14:19:58 +0200 |
wenzelm |
allow type constraints for const_syntax;
|
file |
diff |
annotate
|
| Mon, 14 Oct 2024 11:13:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 14 Oct 2024 11:06:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 22:05:37 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 21:21:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 19:21:47 +0200 |
wenzelm |
tuned: more readable names;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 14:55:46 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 14:48:10 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 14:29:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 06 Oct 2024 18:34:35 +0200 |
wenzelm |
support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
|
file |
diff |
annotate
|
| Thu, 26 Sep 2024 10:51:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2024 13:32:52 +0200 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2024 13:30:04 +0200 |
wenzelm |
minor performance tuning: prefer static values;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2024 13:20:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2024 12:59:43 +0200 |
wenzelm |
clarified persistent datatype: more direct literal_markup, which also serves as a flag;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2024 10:48:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2024 21:13:26 +0200 |
wenzelm |
support for Markup.expression properties in pretty-blocks;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2024 12:10:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2024 11:06:11 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 14:41:45 +0200 |
wenzelm |
tuned signature: separate markup vs. extern;
|
file |
diff |
annotate
|
| Thu, 22 Aug 2024 17:12:32 +0200 |
wenzelm |
tuned: prefer configuration options via context;
|
file |
diff |
annotate
|
| Tue, 19 Jan 2021 20:23:13 +0100 |
wenzelm |
suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff);
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2018 14:58:01 +0200 |
wenzelm |
more liberal: detect free-form infixes as well, e.g. Orderings.ord_class.less_eq;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2018 22:33:20 +0200 |
wenzelm |
more accurate syntax: e.g. avoid brackets as prefix notation;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2018 21:16:24 +0200 |
wenzelm |
more approximative prefix syntax, including binder;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2018 17:04:50 +0200 |
wenzelm |
clarified get_infix: avoid old ASCII input syntax;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 15:07:30 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 16:15:31 +0200 |
wenzelm |
explicit property for unbreakable block;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 23:36:33 +0200 |
wenzelm |
explicit mixfix block properties;
|
file |
diff |
annotate
|
| 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
|