| Tue, 15 Oct 2024 23:44:42 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Thu, 05 Sep 2024 17:39:45 +0200 |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2024 17:58:13 +0200 |
wenzelm |
more conservative cache: retain concurrent value;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2024 11:36:09 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 15 Jul 2024 12:26:15 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2024 20:28:25 +0200 |
wenzelm |
minor performance tuning: more compact data;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 19:51:30 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 09:58:12 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2023 13:35:17 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2023 13:25:06 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2023 12:23:47 +0100 |
wenzelm |
slightly more compact heap: better sharing of persistent tuples;
|
file |
diff |
annotate
|
| Sun, 07 May 2023 12:30:11 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sat, 06 May 2023 13:42:03 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Fri, 05 May 2023 23:48:14 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2023 14:29:52 +0200 |
wenzelm |
minor performance tuning: avoid excessive (de)constructions for base cases;
|
file |
diff |
annotate
|
| Wed, 19 Apr 2023 11:10:52 +0200 |
wenzelm |
unused (see also 864c7c684651 and b6aa5eac0a1a);
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 13:06:43 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 09:49:30 +0200 |
wenzelm |
more compact data: approx. 75% .. 85% of AList size;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 09:01:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 18:16:33 +0200 |
wenzelm |
more Set() and Table() instances;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 14:59:40 +0200 |
wenzelm |
performance tuning: make_size accounts for boxes, i.e. pointer derefs required in "count";
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 13:43:11 +0200 |
wenzelm |
performance tuning;
|
file |
diff |
annotate
|
| Mon, 03 Apr 2023 21:16:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 03 Apr 2023 21:13:46 +0200 |
wenzelm |
clarified signature: more uniform Table() vs. Set();
|
file |
diff |
annotate
|
| Sat, 01 Apr 2023 13:04:59 +0200 |
wenzelm |
tuned: prefer "build" combinator;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 12:25:24 +0200 |
wenzelm |
tuned comments (amending 1951f6470792);
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 12:24:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 12:05:56 +0200 |
wenzelm |
discontinue somewhat pointless is_single, which also depends on details of internal data representation;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 12:02:34 +0200 |
wenzelm |
more compact data: approx. 0.85 .. 1.10 of plain list size;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 10:34:50 +0200 |
wenzelm |
slightly more compact data;
|
file |
diff |
annotate
|