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
|