src/Pure/Syntax/syntax.ML
Fri, 25 Apr 2025 11:22:25 +0200 wenzelm more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
Mon, 27 Jan 2025 18:32:18 +0100 wenzelm more operations;
Mon, 16 Dec 2024 12:55:39 +0100 wenzelm clarified signature;
Sun, 15 Dec 2024 20:12:45 +0100 wenzelm clarified signature (see also 2157039256d3);
Sat, 14 Dec 2024 22:04:39 +0100 wenzelm tuned signature: avoid shadowing;
Sat, 14 Dec 2024 17:35:53 +0100 wenzelm clarified signature;
Sat, 14 Dec 2024 16:58:53 +0100 wenzelm clarified signature and modules;
Fri, 13 Dec 2024 23:23:07 +0100 wenzelm minor performance tuning: avoid excessive Library.insert and Symbol.explode operations;
Wed, 16 Oct 2024 21:22:37 +0200 wenzelm clarified signature: more explicit Syntax.print_mode_tabs, depending on print_mode_value ();
Mon, 14 Oct 2024 11:16:11 +0200 wenzelm tuned;
Sat, 12 Oct 2024 14:22:19 +0200 wenzelm clarified signature;
Sat, 05 Oct 2024 14:58:36 +0200 wenzelm first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
less more (0) -300 -100 -12 tip