| 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
|
| Tue, 28 Mar 2023 22:46:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 22:43:05 +0200 |
wenzelm |
more compact representation of leaf nodes: only 1.10 .. 1.33 larger than plain list;
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 19:43:49 +0200 |
wenzelm |
tuned --- fewer compiler warnings;
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 19:07:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 19:03:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 18:10:45 +0200 |
wenzelm |
tuned signature: more uniform structure Key;
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 17:30:39 +0200 |
wenzelm |
tuned names: "e" means "entry" in table.ML and "elem" in set.ML;
|
file |
diff |
annotate
|
| Mon, 27 Mar 2023 16:24:54 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 14:50:26 +0200 |
wenzelm |
clarified set of items with order of addition;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 13:49:26 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 14:20:39 +0100 |
wenzelm |
performance fine-tuning of hot spot;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 16:05:33 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 29 Jan 2018 22:25:07 +0100 |
wenzelm |
clarified operations;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2017 19:39:03 +0100 |
wenzelm |
more recent polyml-test version;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 23:47:07 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 11:59:03 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 20:56:34 +0100 |
wenzelm |
clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 13:58:22 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 19:44:09 +0100 |
wenzelm |
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
|
file |
diff |
annotate
|
| Fri, 17 May 2013 13:46:18 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 20:09:51 +0100 |
wenzelm |
convenience operations for table as set;
|
file |
diff |
annotate
|
| Thu, 24 May 2012 15:33:45 +0200 |
wenzelm |
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 22:28:53 +0200 |
wenzelm |
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 16:42:14 +0200 |
wenzelm |
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 15:11:41 +0200 |
wenzelm |
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
|
file |
diff |
annotate
|
| Sat, 06 Feb 2010 16:32:34 +0100 |
wenzelm |
removed unused "boundary" of Table/Graph.get_first;
|
file |
diff |
annotate
|