| Wed, 27 Apr 2011 17:44:06 +0200 |
wenzelm |
export Name_Space.entry_ord;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 17:02:12 +0200 |
wenzelm |
added Name_Space.check/get convenience;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:04:22 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 11 Apr 2011 17:11:03 +0200 |
wenzelm |
Name_Space.entry_markup: keep def position as separate properties;
|
file |
diff |
annotate
|
| Sun, 27 Mar 2011 20:55:01 +0200 |
wenzelm |
decode_term: some context-sensitive markup;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 22:23:56 +0100 |
wenzelm |
extra checking of name bindings for classes, types, consts;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:27:35 +0100 |
wenzelm |
added Name_Space.alias -- additional accesses for an existing entry;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:33:33 +0100 |
wenzelm |
removed unused external_names;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 20:46:46 +0100 |
wenzelm |
more systematic treatment of qualified names derived from binding;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 14:50:55 +0100 |
wenzelm |
uniform new_group/reset_group;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 17:36:34 +0100 |
wenzelm |
let naming transform binding beforehand -- covering only the "conceal" flag for now;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:14:46 +0100 |
wenzelm |
Name_Space.naming: maintain group and theory_name as well;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 12:27:21 +0100 |
wenzelm |
allow name space entries to be "concealed" -- via binding/naming/local_theory;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 21:30:33 +0200 |
wenzelm |
maintain position of formal entities via name space;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 20:54:08 +0200 |
wenzelm |
maintain explicit name space kind;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:04:57 +0200 |
wenzelm |
maintain abstract entry, with position, identity etc.;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:09:37 +0200 |
haftmann |
curried inter as canonical list operation (beware of argument order)
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Sat, 14 Mar 2009 00:13:50 +0100 |
wenzelm |
removed obsolete no_base_names naming policy;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 13:18:42 +0100 |
wenzelm |
renamed sticky_prefix to mandatory_path;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 11:09:26 +0100 |
wenzelm |
renamed bind to define;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 10 Mar 2009 21:18:01 +0100 |
wenzelm |
add_path: discontinued special meaning of "//", "/", "..";
|
file |
diff |
annotate
|
| Tue, 10 Mar 2009 16:51:08 +0100 |
wenzelm |
just one naming policy based on binding content -- eliminated odd "object-oriented" style;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 16:53:07 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 10:53:49 +0100 |
wenzelm |
adapted Binding.dest;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 21:53:52 +0100 |
wenzelm |
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:53:29 +0100 |
wenzelm |
moved name space externalization flags back to name_space.ML;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 17:25:07 +1100 |
Timothy Bourke |
Nicer names in FindTheorems.
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Sat, 03 Jan 2009 08:39:18 +0100 |
haftmann |
separator, is_qualified
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:42:37 +0100 |
haftmann |
removed Table.extend, NameSpace.extend_table
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 12:17:01 +0100 |
haftmann |
exported get_accesses (for diagnostic purpose)
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:51:40 +0100 |
haftmann |
name spaces and name bindings
|
file |
diff |
annotate
|
| Fri, 13 Jun 2008 21:04:43 +0200 |
wenzelm |
hide: delete all accesses from extra names -- reduces ambiguity in extern;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:16 +0200 |
wenzelm |
merge: canonical order;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 17:35:57 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Mon, 29 Oct 2007 16:13:44 +0100 |
wenzelm |
export is_hidden;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2007 23:16:33 +0200 |
wenzelm |
store external accesses within name space (as produced by naming policy);
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 20:44:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 22:40:57 +0200 |
wenzelm |
declare: disallow quote (") in names;
|
file |
diff |
annotate
|
| Thu, 24 May 2007 08:37:37 +0200 |
haftmann |
tuned Pure/General/name_space.ML
|
file |
diff |
annotate
|
| Wed, 10 Jan 2007 20:17:26 +0100 |
wenzelm |
removed NameSpace.split -- use qualifier/base instead;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:10:05 +0100 |
haftmann |
added split
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 21:41:25 +0200 |
wenzelm |
renamed NameSpace.drop_base to NameSpace.qualifier;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:06 +0100 |
wenzelm |
removed qualified_force_prefix;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:24 +0100 |
wenzelm |
low-level tuning of merge: maintain identity of accesses;
|
file |
diff |
annotate
|
| Sat, 11 Feb 2006 17:17:50 +0100 |
wenzelm |
removed custom_accesses;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:06 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 16:35:40 +0200 |
haftmann |
cleaned up nth, nth_update, nth_map and nth_string functions
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2005 16:04:47 +0200 |
wenzelm |
removed unused dest operation;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:32 +0200 |
wenzelm |
added dest_table;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:29 +0200 |
wenzelm |
Symtab.fold;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 12:03:28 +0200 |
wenzelm |
added type NameSpace.table with basic operations;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 11:31:25 +0200 |
wenzelm |
no warning for non-identifiers;
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:28 +0200 |
wenzelm |
renamed cond_extern to extern;
|
file |
diff |
annotate
|
| Wed, 18 May 2005 11:30:59 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 17:03:37 +0100 |
ballarin |
Further work on interpretation commands. New command `interpret' for
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Tue, 06 Jul 2004 20:31:37 +0200 |
schirmer |
added flag unique_names
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Wed, 11 Feb 2004 17:36:08 +0100 |
berghofe |
Added flag short_names
|
file |
diff |
annotate
|
| Mon, 22 Sep 2003 16:19:46 +0200 |
berghofe |
Modified merge_aux to prevent newer names from getting overwritten
|
file |
diff |
annotate
|
| Wed, 10 Jul 2002 14:47:48 +0200 |
wenzelm |
added accesses';
|
file |
diff |
annotate
|
| Fri, 21 Dec 2001 23:17:12 +0100 |
wenzelm |
hide: flag for full/base name;
|
file |
diff |
annotate
|
| Tue, 20 Nov 2001 20:57:07 +0100 |
wenzelm |
moved prefixes1, suffixes1 to library.ML;
|
file |
diff |
annotate
|
| Thu, 18 Oct 2001 21:02:46 +0200 |
wenzelm |
added map_base;
|
file |
diff |
annotate
|
| Sun, 25 Jun 2000 23:46:03 +0200 |
wenzelm |
export hidden: string -> string;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:02:46 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2000 14:10:38 +0200 |
wenzelm |
improved output of ambiguous entries;
|
file |
diff |
annotate
|
| Mon, 28 Jun 1999 21:38:50 +0200 |
wenzelm |
added cond_extern_table;
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 15:18:02 +0100 |
wenzelm |
fixed titles;
|
file |
diff |
annotate
|
| Tue, 20 Oct 1998 16:20:19 +0200 |
wenzelm |
Symtab.foldl;
|
file |
diff |
annotate
|
| Wed, 22 Jul 1998 17:59:49 +0200 |
wenzelm |
moved long_names / cond_extern to name_space.ML;
|
file |
diff |
annotate
|
| Wed, 10 Jun 1998 11:51:58 +0200 |
wenzelm |
moved name_space.ML to General/name_space.ML;
|
file |
diff |
annotate
|