* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
Tue, 05 Jul 2005 14:07:08 +0200
changeset 16689 05b986733a59
parent 16688 e3de7ea24c23
child 16690 b8b2579a2509
* Pure: structure OrdList (cf. Pure/General/ord_list.ML); * Pure: more efficient orders for basic syntactic entities;
--- a/NEWS	Tue Jul 05 13:57:23 2005 +0200
+++ b/NEWS	Tue Jul 05 14:07:08 2005 +0200
@@ -415,6 +415,17 @@
 Poly/ML, set to 1 to profile time, 2 to profile space (which increases
 the runtime).
+* Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
+reasonably efficient light-weight implementation of lists as sets.
+* Pure: more efficient orders for basic syntactic entities: added
+fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord
+and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is
+NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast
+orders now -- potential INCOMPATIBILITY for code that depends on a
+particular order for Symtab.keys, Symtab.dest, etc. (consider using
+Library.sort_strings on result).
 * Pure: name spaces have been refined, with significant changes of the
 internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)
 to extern(_table).  The plain name entry path is superceded by a