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