Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/General/table.ML
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
Sun, 25 Oct 2009 19:14:11 +0100 wenzelm merge_list: no exception DUP here; file | diff | annotate
Thu, 09 Jul 2009 22:01:41 +0200 wenzelm renamed functor TableFun to Table, and GraphFun to Graph; file | diff | annotate
Sun, 14 Jun 2009 03:02:25 +0200 wenzelm improved correctness of get_first (boundary check); file | diff | annotate
Sat, 13 Jun 2009 22:01:33 +0200 wenzelm improved get_first: check boundary before entering subtrees; file | diff | annotate
Sat, 13 Jun 2009 19:19:14 +0200 wenzelm native get_first, with optional boundary; file | diff | annotate
Wed, 20 May 2009 10:37:38 +0200 haftmann dropped parentheses file | diff | annotate
Sun, 22 Mar 2009 11:56:22 +0100 haftmann added Symreltab (binary relations of symbols) instance of TableFun file | diff | annotate
Thu, 05 Mar 2009 20:55:28 +0100 wenzelm removed unused TableFun().fold_map and GraphFun().fold_map_nodes; file | diff | annotate
Thu, 05 Mar 2009 15:25:35 +0100 wenzelm TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion; file | diff | annotate
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids; file | diff | annotate
Fri, 05 Dec 2008 18:42:37 +0100 haftmann removed Table.extend, NameSpace.extend_table file | diff | annotate
Tue, 23 Sep 2008 17:28:58 +0200 wenzelm added fold_rev; file | diff | annotate
Thu, 07 Aug 2008 21:07:57 +0200 wenzelm map_default: more explicit scope; file | diff | annotate
Wed, 09 Jul 2008 17:14:31 +0200 wenzelm added get_first; file | diff | annotate
Sun, 11 Nov 2007 14:00:10 +0100 wenzelm renamed update_list to cons_list; file | diff | annotate
Sun, 08 Jul 2007 19:51:58 +0200 wenzelm replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP; file | diff | annotate
Fri, 20 Oct 2006 10:44:51 +0200 haftmann abandoned foldl file | diff | annotate
Tue, 18 Jul 2006 08:48:11 +0200 haftmann added Table.map_default file | diff | annotate
Thu, 13 Jul 2006 13:42:05 +0200 wenzelm tuned insert_list; file | diff | annotate
Sat, 29 Apr 2006 23:16:48 +0200 wenzelm added insert_list; file | diff | annotate
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter); file | diff | annotate
Thu, 16 Feb 2006 18:25:56 +0100 wenzelm removed pointless replace; file | diff | annotate
Sun, 12 Feb 2006 21:34:25 +0100 wenzelm export exception SAME (for join); file | diff | annotate
Mon, 06 Feb 2006 20:59:46 +0100 wenzelm renamed xxx_multi to xxx_list; file | diff | annotate
Fri, 28 Oct 2005 09:35:04 +0200 haftmann removed obfuscating PStrStrTab file | diff | annotate
Wed, 19 Oct 2005 17:21:53 +0200 haftmann added table functor instance for pairs of strings file | diff | annotate
Thu, 29 Sep 2005 00:59:02 +0200 wenzelm tuned default operation: use internal modify; file | diff | annotate
Thu, 22 Sep 2005 07:56:04 +0200 haftmann added fold_map_table file | diff | annotate
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update; file | diff | annotate
Thu, 01 Sep 2005 18:48:54 +0200 wenzelm added curried_lookup/update operations -- in preparation of currying plain lookup/update; file | diff | annotate
Mon, 29 Aug 2005 08:34:24 +0200 haftmann canonical interface for 'default' file | diff | annotate
Thu, 25 Aug 2005 09:23:13 +0200 haftmann added 'default' function file | diff | annotate
Tue, 19 Jul 2005 20:47:01 +0200 wenzelm Inttab.defined; file | diff | annotate
Tue, 19 Jul 2005 17:21:59 +0200 wenzelm added defined; file | diff | annotate
Fri, 15 Jul 2005 15:44:19 +0200 wenzelm tuned min_key, max_key; file | diff | annotate
Tue, 05 Jul 2005 13:55:09 +0200 wenzelm Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.; file | diff | annotate
Fri, 01 Jul 2005 14:42:01 +0200 wenzelm low-level tuning of map, fold; file | diff | annotate
Sat, 18 Jun 2005 22:42:01 +0200 wenzelm added member; file | diff | annotate
Fri, 17 Jun 2005 18:33:31 +0200 wenzelm added map', fold; file | diff | annotate
Thu, 09 Jun 2005 12:03:29 +0200 wenzelm added structure Inttab; file | diff | annotate
Thu, 02 Jun 2005 18:29:52 +0200 wenzelm exists: made non-strict; file | diff | annotate
Tue, 31 May 2005 11:53:30 +0200 wenzelm remove(_multi): generalized type; file | diff | annotate
Wed, 18 May 2005 11:30:59 +0200 wenzelm tuned; file | diff | annotate
Sun, 17 Apr 2005 19:40:34 +0200 wenzelm added delete_safe, insert, remove, remove_multi; file | diff | annotate
Thu, 07 Apr 2005 09:26:40 +0200 wenzelm tuned updates, added map_entry; file | diff | annotate
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr. file | diff | annotate
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions. file | diff | annotate
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type. file | diff | annotate
Tue, 24 Aug 2004 17:55:24 +0200 obua changes file | diff | annotate
Sat, 03 Jul 2004 15:26:58 +0200 berghofe Added delete operation. file | diff | annotate
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004 file | diff | annotate
Sat, 24 Nov 2001 16:58:31 +0100 wenzelm added join, merge_multi('); file | diff | annotate
Fri, 05 May 2000 22:02:46 +0200 wenzelm GPLed; file | diff | annotate
Thu, 30 Mar 2000 14:18:40 +0200 wenzelm export update_multi; file | diff | annotate
Fri, 10 Mar 2000 15:00:32 +0100 berghofe Added function min_key. file | diff | annotate
Thu, 22 Jul 1999 20:52:58 +0200 wenzelm added exists; file | diff | annotate
Wed, 13 Jan 1999 15:18:02 +0100 wenzelm fixed titles; file | diff | annotate
Tue, 20 Oct 1998 16:19:53 +0200 wenzelm added foldl, keys; file | diff | annotate
Wed, 10 Jun 1998 11:53:37 +0200 wenzelm moved table.ML to General/table.ML; file | diff | annotate
less more (0) tip
isabelle