| Sun, 27 Jul 2025 16:28:10 +0200 |
wenzelm |
more direct support for "command_span" markup property "is_begin";
|
file |
diff |
annotate
|
| Thu, 24 Apr 2025 22:45:04 +0200 |
wenzelm |
more scalable;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2025 18:37:05 +0100 |
wenzelm |
support for writeln_urgent, which is shown in Output before state messages (reminiscent of old Output.urgent_message before 521cea5fa777);
|
file |
diff |
annotate
|
| Thu, 06 Feb 2025 12:46:13 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 08 Dec 2024 20:09:14 +0100 |
wenzelm |
more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;
|
file |
diff |
annotate
|
| Sat, 07 Dec 2024 23:50:18 +0100 |
wenzelm |
clarified term positions and markup: syntax = true means this is via concrete syntax;
|
file |
diff |
annotate
|
| Sun, 27 Oct 2024 11:13:42 +0100 |
wenzelm |
clarified symbolic output: avoid redundant "block" element for open_block = true;
|
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
|
| Sun, 06 Oct 2024 13:02:33 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 29 Sep 2024 12:09:49 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Sun, 22 Sep 2024 16:04:44 +0200 |
wenzelm |
remove specific support for "expression" block markup: prefer "notation";
|
file |
diff |
annotate
|
| Sun, 22 Sep 2024 15:46:19 +0200 |
wenzelm |
more uniform treatment of Markup.notation and Markup.expression: manage kinds via context;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 18:09:04 +0200 |
wenzelm |
support more markup elements;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 15:35:16 +0200 |
wenzelm |
block markup for specific notation, notably infix and binder;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 13:30:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2024 21:13:26 +0200 |
wenzelm |
support for Markup.expression properties in pretty-blocks;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2024 13:09:26 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2024 21:25:15 +0200 |
wenzelm |
dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";
|
file |
diff |
annotate
|
| Wed, 11 Sep 2024 20:05:09 +0200 |
wenzelm |
more robust: global ML name space for markup elements;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2024 19:57:45 +0200 |
wenzelm |
clarified print mode "latex": no longer impact Output/Markup/Pretty operations;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 19:51:16 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 19:40:18 +0200 |
wenzelm |
prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process");
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 11:41:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 11:12:13 +0200 |
wenzelm |
clarified signature: more explicit type "ops";
|
file |
diff |
annotate
|
| Thu, 29 Aug 2024 17:47:29 +0200 |
wenzelm |
more scalable pretty printing: avoid exception String.Size at command "value" (line 33 of "$AFP/Iptables_Semantics/Examples/SQRL_Shorewall/Analyze_SQRL_Shorewall.thy") in AFP/c69af9cd3390;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2023 16:30:14 +0200 |
wenzelm |
clarified signature: systematic use of Properties.make_string;
|
file |
diff |
annotate
|
| Sun, 09 Jul 2023 17:39:46 +0200 |
wenzelm |
more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;
|
file |
diff |
annotate
|
| Wed, 10 May 2023 20:30:46 +0200 |
wenzelm |
more informative position information;
|
file |
diff |
annotate
|
| Sat, 01 Apr 2023 14:59:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 20 Jan 2023 19:52:52 +0100 |
wenzelm |
more direct check of bibtex entries via Isabelle/Scala;
|
file |
diff |
annotate
|