| 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
|