src/Pure/General/name_space.ML
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-12-01 haftmann 2008-12-01 exported get_accesses (for diagnostic purpose)
2008-11-20 haftmann 2008-11-20 name spaces and name bindings
2008-06-13 wenzelm 2008-06-13 hide: delete all accesses from extra names -- reduces ambiguity in extern;
2008-04-15 wenzelm 2008-04-15 merge: canonical order;
2008-03-27 wenzelm 2008-03-27 tuned comments; tuned;
2007-10-29 wenzelm 2007-10-29 export is_hidden;
2007-10-17 wenzelm 2007-10-17 store external accesses within name space (as produced by naming policy); improved sticky_prefix: suppress redundant accesses to achieve shorter output; removed unused interfaces; replaced accesses' by external_names (depening on naming);
2007-08-20 wenzelm 2007-08-20 tuned signature;
2007-07-09 wenzelm 2007-07-09 declare: disallow quote (") in names;
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-01-10 wenzelm 2007-01-10 removed NameSpace.split -- use qualifier/base instead;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-27 haftmann 2006-12-27 added split
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-09-13 wenzelm 2006-09-13 renamed NameSpace.drop_base to NameSpace.qualifier;
2006-04-08 wenzelm 2006-04-08 tuned;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-15 wenzelm 2006-02-15 removed qualified_force_prefix; added sticky_prefix;
2006-02-12 wenzelm 2006-02-12 low-level tuning of merge: maintain identity of accesses; simplified TableFun.join;
2006-02-11 wenzelm 2006-02-11 removed custom_accesses; added suffixes_prefixes_split, qualified_force_prefix;
2006-02-06 wenzelm 2006-02-06 tuned;
2005-10-28 haftmann 2005-10-28 cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-28 wenzelm 2005-08-28 removed unused dest operation;
2005-07-14 wenzelm 2005-07-14 added dest_table;
2005-06-17 wenzelm 2005-06-17 Symtab.fold;
2005-06-09 wenzelm 2005-06-09 added type NameSpace.table with basic operations;
2005-06-05 wenzelm 2005-06-05 no warning for non-identifiers;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; append, base, drop_base, map_base: made robust against empty names; added qualified; extern: improved output for non-unique non-hidden names; name entry path superceded by general naming context; added reject_qualified, default_naming, add_path, no_base_names, custom_accesses, set_policy;
2005-05-18 wenzelm 2005-05-18 tuned;
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-07-06 schirmer 2004-07-06 added flag unique_names
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-02-11 berghofe 2004-02-11 Added flag short_names
2003-09-22 berghofe 2003-09-22 Modified merge_aux to prevent newer names from getting overwritten by older names.
2002-07-10 wenzelm 2002-07-10 added accesses';
2001-12-21 wenzelm 2001-12-21 hide: flag for full/base name;
2001-11-20 wenzelm 2001-11-20 moved prefixes1, suffixes1 to library.ML;
2001-10-18 wenzelm 2001-10-18 added map_base;
2000-06-25 wenzelm 2000-06-25 export hidden: string -> string;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-17 wenzelm 2000-04-17 improved output of ambiguous entries; support hiding;
1999-06-28 wenzelm 1999-06-28 added cond_extern_table;
1999-01-13 wenzelm 1999-01-13 fixed titles;
1998-10-20 wenzelm 1998-10-20 Symtab.foldl;
1998-07-22 wenzelm 1998-07-22 moved long_names / cond_extern to name_space.ML;
1998-06-10 wenzelm 1998-06-10 moved name_space.ML to General/name_space.ML;