| Tue, 12 Nov 2024 22:30:45 +0100 |
wenzelm |
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
|
file |
diff |
annotate
|
| Mon, 11 Nov 2024 13:15:55 +0100 |
wenzelm |
minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 22:22:34 +0100 |
wenzelm |
clarified signature: absorb XZ.Cache into XML.Cache;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 16:12:52 +0100 |
wenzelm |
clarified boundary case;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 15:58:48 +0100 |
wenzelm |
clarified signature --- internal Cache.none;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 14:24:03 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 15 Jan 2020 19:49:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:26:50 +0200 |
wenzelm |
clarified type Indexname, with plain value Int;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 14:18:31 +0200 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
| Thu, 24 May 2018 21:21:26 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Thu, 24 May 2018 21:13:09 +0200 |
wenzelm |
more general cache, also for term substructures;
|
file |
diff |
annotate
|