| Fri, 13 Dec 2024 23:23:07 +0100 |
wenzelm |
minor performance tuning: avoid excessive Library.insert and Symbol.explode operations;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 17:40:15 +0100 |
wenzelm |
clarified signature: shorten common cases;
|
file |
diff |
annotate
|
| Tue, 22 Oct 2024 12:03:46 +0200 |
wenzelm |
clarified markers for syntax consts: avoid overlap with logical consts;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2024 22:05:37 +0200 |
wenzelm |
misc tuning and clarification;
|
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, 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
|
| Sun, 22 Sep 2024 14:41:34 +0200 |
wenzelm |
clarified modules and signature;
|
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
|
| Fri, 20 Sep 2024 11:19:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 11:10:04 +0200 |
wenzelm |
no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);
|
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 20:56:47 +0200 |
wenzelm |
more positions;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2024 12:08:56 +0200 |
wenzelm |
proper Context_Position.report, following 5328d67ec647;
|
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
|
| Tue, 17 Sep 2024 11:32:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2024 11:14:25 +0200 |
wenzelm |
unused (see 39261908e12f);
|
file |
diff |
annotate
|
| Tue, 17 Sep 2024 11:06:11 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2024 10:47:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 16 Sep 2024 19:58:28 +0200 |
wenzelm |
more formal Markup.expression;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 18:38:44 +0200 |
wenzelm |
support for syntax const dependencies, with minimal integrity checks;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 00:41:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2020 16:04:27 +0100 |
wenzelm |
allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 20:16:42 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2018 17:04:50 +0200 |
wenzelm |
clarified get_infix: avoid old ASCII input syntax;
|
file |
diff |
annotate
|
| Sun, 16 Sep 2018 22:45:34 +0200 |
wenzelm |
export plain infix syntax;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 10:39:50 +0100 |
wenzelm |
more uniform treatment of "bad" like other messages (with serial number);
|
file |
diff |
annotate
|
| Wed, 21 Sep 2016 22:43:06 +0200 |
wenzelm |
more general mixfix delimiters;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|