src/Pure/General/name_space.ML
Wed, 27 Apr 2011 17:44:06 +0200 wenzelm export Name_Space.entry_ord;
Sat, 23 Apr 2011 17:02:12 +0200 wenzelm added Name_Space.check/get convenience;
Sun, 17 Apr 2011 21:04:22 +0200 wenzelm tuned signature;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Mon, 11 Apr 2011 17:11:03 +0200 wenzelm Name_Space.entry_markup: keep def position as separate properties;
Sun, 27 Mar 2011 20:55:01 +0200 wenzelm decode_term: some context-sensitive markup;
Fri, 17 Dec 2010 22:23:56 +0100 wenzelm extra checking of name bindings for classes, types, consts;
Tue, 09 Mar 2010 23:27:35 +0100 wenzelm added Name_Space.alias -- additional accesses for an existing entry;
Wed, 03 Mar 2010 00:33:33 +0100 wenzelm removed unused external_names;
Thu, 18 Feb 2010 20:46:46 +0100 wenzelm more systematic treatment of qualified names derived from binding;
Tue, 17 Nov 2009 14:50:55 +0100 wenzelm uniform new_group/reset_group;
Wed, 28 Oct 2009 17:36:34 +0100 wenzelm let naming transform binding beforehand -- covering only the "conceal" flag for now;
Sun, 25 Oct 2009 19:14:46 +0100 wenzelm Name_Space.naming: maintain group and theory_name as well;
Sun, 25 Oct 2009 12:27:21 +0100 wenzelm allow name space entries to be "concealed" -- via binding/naming/local_theory;
Sat, 24 Oct 2009 21:30:33 +0200 wenzelm maintain position of formal entities via name space;
Sat, 24 Oct 2009 20:54:08 +0200 wenzelm maintain explicit name space kind;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 24 Oct 2009 19:04:57 +0200 wenzelm maintain abstract entry, with position, identity etc.;
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 14 Mar 2009 00:13:50 +0100 wenzelm removed obsolete no_base_names naming policy;
Thu, 12 Mar 2009 13:18:42 +0100 wenzelm renamed sticky_prefix to mandatory_path;
Thu, 12 Mar 2009 11:09:26 +0100 wenzelm renamed bind to define;
Wed, 11 Mar 2009 16:36:27 +0100 wenzelm 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);
Tue, 10 Mar 2009 21:18:01 +0100 wenzelm add_path: discontinued special meaning of "//", "/", "..";
Tue, 10 Mar 2009 16:51:08 +0100 wenzelm just one naming policy based on binding content -- eliminated odd "object-oriented" style;
Sun, 08 Mar 2009 16:53:07 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Thu, 05 Mar 2009 10:53:49 +0100 wenzelm adapted Binding.dest;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 21:53:52 +0100 wenzelm eliminated internal stamp equality, replaced by bare-metal pointer_eq;
Tue, 03 Mar 2009 18:31:59 +0100 wenzelm moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
Tue, 03 Mar 2009 14:53:29 +0100 wenzelm moved name space externalization flags back to name_space.ML;
Tue, 03 Mar 2009 14:16:05 +0100 wenzelm 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);
Mon, 09 Feb 2009 17:25:07 +1100 Timothy Bourke Nicer names in FindTheorems.
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Sat, 03 Jan 2009 08:39:18 +0100 haftmann separator, is_qualified
Fri, 05 Dec 2008 18:42:37 +0100 haftmann removed Table.extend, NameSpace.extend_table
Fri, 05 Dec 2008 08:04:53 +0100 haftmann dropped NameSpace.declare_base
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Mon, 01 Dec 2008 19:41:16 +0100 haftmann new Binding module
Mon, 01 Dec 2008 12:17:01 +0100 haftmann exported get_accesses (for diagnostic purpose)
Thu, 20 Nov 2008 14:51:40 +0100 haftmann name spaces and name bindings
Fri, 13 Jun 2008 21:04:43 +0200 wenzelm hide: delete all accesses from extra names -- reduces ambiguity in extern;
Tue, 15 Apr 2008 16:12:16 +0200 wenzelm merge: canonical order;
Thu, 27 Mar 2008 17:35:57 +0100 wenzelm tuned comments;
Mon, 29 Oct 2007 16:13:44 +0100 wenzelm export is_hidden;
Wed, 17 Oct 2007 23:16:33 +0200 wenzelm store external accesses within name space (as produced by naming policy);
Mon, 20 Aug 2007 20:44:01 +0200 wenzelm tuned signature;
Mon, 09 Jul 2007 22:40:57 +0200 wenzelm declare: disallow quote (") in names;
Thu, 24 May 2007 08:37:37 +0200 haftmann tuned Pure/General/name_space.ML
Wed, 10 Jan 2007 20:17:26 +0100 wenzelm removed NameSpace.split -- use qualifier/base instead;
Sat, 30 Dec 2006 16:08:00 +0100 wenzelm removed conditional combinator;
Wed, 27 Dec 2006 19:10:05 +0100 haftmann added split
Fri, 15 Dec 2006 00:08:06 +0100 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
Wed, 13 Sep 2006 21:41:25 +0200 wenzelm renamed NameSpace.drop_base to NameSpace.qualifier;
less more (0) -60 tip