src/Pure/General/name_space.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-03-14 wenzelm 2009-03-14 removed obsolete no_base_names naming policy;
2009-03-12 wenzelm 2009-03-12 renamed sticky_prefix to mandatory_path;
2009-03-12 wenzelm 2009-03-12 renamed bind to define; misc tuning and polishing;
2009-03-11 wenzelm 2009-03-11 eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-03-10 wenzelm 2009-03-10 add_path: discontinued special meaning of "//", "/", ".."; added root_path, parent_path;
2009-03-10 wenzelm 2009-03-10 just one naming policy based on binding content -- eliminated odd "object-oriented" style; uniform handling of regular vs. mandatory name prefixes -- add_path and sticky_prefix may be freely intermixed; misc tuning and cleanup;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name; tuned signature;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-05 wenzelm 2009-03-05 adapted Binding.dest; tuned;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 eliminated internal stamp equality, replaced by bare-metal pointer_eq; misc tuning and polishing;
2009-03-03 wenzelm 2009-03-03 moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings; moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names; type binding: maintain explicit qualifier, indepently of base name; tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused); Binding.str_of: include markup with position properties; misc tuning;
2009-03-03 wenzelm 2009-03-03 moved name space externalization flags back to name_space.ML; added pure version extern_flags; do not export internal get_accesses;
2009-03-03 wenzelm 2009-03-03 reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
2009-02-09 Timothy Bourke 2009-02-09 Nicer names in FindTheorems. * Patch NameSpace.get_accesses, contributed by Timothy Bourke: NameSpace.get_accesses has been patched to fix the following bug: theory OverHOL imports Main begin lemma conjI: "a & b --> b" by blast ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of; val x1 = NameSpace.get_accesses ns "HOL.conjI"; val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *} end where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"], but x1 should be just ["HOL.conjI"]. NameSpace.get_accesses is only used within the NameSpace structure itself. The two uses have been modified to retain their original behaviour. Note that NameSpace.valid_accesses gives different results: get_accesses ns "HOL.eq_class.eq" gives ["eq", "eq_class.eq", "HOL.eq_class.eq"] but, valid_accesses ns "HOL.eq_class.eq" gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"] * Patch FindTheorems: Prefer names that are shorter to type in the current context. * Re-export space_of.
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-03 haftmann 2009-01-03 separator, is_qualified
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.