| Fri, 25 Apr 2025 11:22:25 +0200 |
wenzelm |
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 18:32:18 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 16 Dec 2024 12:55:39 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 15 Dec 2024 20:12:45 +0100 |
wenzelm |
clarified signature (see also 2157039256d3);
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 22:04:39 +0100 |
wenzelm |
tuned signature: avoid shadowing;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 17:35:53 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 16:58:53 +0100 |
wenzelm |
clarified signature and modules;
|
file |
diff |
annotate
|
| Fri, 13 Dec 2024 23:23:07 +0100 |
wenzelm |
minor performance tuning: avoid excessive Library.insert and Symbol.explode operations;
|
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
|
| Mon, 14 Oct 2024 11:16:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 14:22:19 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 05 Oct 2024 14:58:36 +0200 |
wenzelm |
first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
|
file |
diff |
annotate
|
| Sun, 29 Sep 2024 20:11:28 +0200 |
wenzelm |
clarified order for 'print_syntax' command;
|
file |
diff |
annotate
|
| Sat, 28 Sep 2024 20:28:11 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2024 17:51:55 +0200 |
wenzelm |
more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 20:54:20 +0200 |
wenzelm |
clarified Syntax.is_const (after 43c4817375bf): exclude logical consts from 'syntax_consts' / 'syntax_types', e.g. relevant for @{syntax_const} antiquotation;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 21:32:09 +0200 |
wenzelm |
more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 18:38:44 +0200 |
wenzelm |
support for syntax const dependencies, with minimal integrity checks;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 13:28:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 22 Aug 2024 15:57:30 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Tue, 02 Apr 2024 17:20:09 +0200 |
wenzelm |
further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 23:56:40 +0200 |
wenzelm |
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 21:50:04 +0200 |
wenzelm |
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
|
file |
diff |
annotate
|
| Tue, 09 May 2023 21:32:03 +0200 |
wenzelm |
performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
|
file |
diff |
annotate
|
| Thu, 08 Sep 2022 12:52:41 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2019 21:18:26 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2019 11:41:39 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 24 Mar 2019 19:17:42 +0100 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 21:48:05 +0100 |
wenzelm |
support for isabelle update -u inner_syntax_cartouches;
|
file |
diff |
annotate
|