| Tue, 29 Sep 2009 11:49:22 +0200 |
explicit indication of Unsynchronized.ref;
|
file | diff | annotate |
| Sat, 14 Mar 2009 00:13:50 +0100 |
removed obsolete no_base_names naming policy;
|
file | diff | annotate |
| Thu, 12 Mar 2009 13:18:42 +0100 |
renamed sticky_prefix to mandatory_path;
|
file | diff | annotate |
| Thu, 12 Mar 2009 11:09:26 +0100 |
renamed bind to define;
|
file | diff | annotate |
| Wed, 11 Mar 2009 16:36:27 +0100 |
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 |
add_path: discontinued special meaning of "//", "/", "..";
|
file | diff | annotate |
| Tue, 10 Mar 2009 16:51:08 +0100 |
just one naming policy based on binding content -- eliminated odd "object-oriented" style;
|
file | diff | annotate |
| Sun, 08 Mar 2009 16:53:07 +0100 |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file | diff | annotate |
| Thu, 05 Mar 2009 12:08:00 +0100 |
renamed NameSpace.base to NameSpace.base_name;
|
file | diff | annotate |
| Thu, 05 Mar 2009 10:53:49 +0100 |
adapted Binding.dest;
|
file | diff | annotate |
| Wed, 04 Mar 2009 11:05:29 +0100 |
Merge.
|
file | diff | annotate |
| Wed, 04 Mar 2009 10:45:52 +0100 |
Merge.
|
file | diff | annotate |
| Tue, 03 Mar 2009 21:53:52 +0100 |
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
|
file | diff | annotate |
| Tue, 03 Mar 2009 18:31:59 +0100 |
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 |
moved name space externalization flags back to name_space.ML;
|
file | diff | annotate |
| Tue, 03 Mar 2009 14:16:05 +0100 |
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 |
Nicer names in FindTheorems.
|
file | diff | annotate |
| Wed, 21 Jan 2009 16:47:32 +0100 |
binding is alias for Binding.T
|
file | diff | annotate |
| Sat, 03 Jan 2009 08:39:18 +0100 |
separator, is_qualified
|
file | diff | annotate |
| Fri, 05 Dec 2008 18:42:37 +0100 |
removed Table.extend, NameSpace.extend_table
|
file | diff | annotate |
| Fri, 05 Dec 2008 08:04:53 +0100 |
dropped NameSpace.declare_base
|
file | diff | annotate |
| Thu, 04 Dec 2008 14:43:33 +0100 |
cleaned up binding module and related code
|
file | diff | annotate |
| Mon, 01 Dec 2008 19:41:16 +0100 |
new Binding module
|
file | diff | annotate |
| Mon, 01 Dec 2008 12:17:01 +0100 |
exported get_accesses (for diagnostic purpose)
|
file | diff | annotate |
| Thu, 20 Nov 2008 14:51:40 +0100 |
name spaces and name bindings
|
file | diff | annotate |
| Fri, 13 Jun 2008 21:04:43 +0200 |
hide: delete all accesses from extra names -- reduces ambiguity in extern;
|
file | diff | annotate |
| Tue, 15 Apr 2008 16:12:16 +0200 |
merge: canonical order;
|
file | diff | annotate |
| Thu, 27 Mar 2008 17:35:57 +0100 |
tuned comments;
|
file | diff | annotate |
| Mon, 29 Oct 2007 16:13:44 +0100 |
export is_hidden;
|
file | diff | annotate |
| Wed, 17 Oct 2007 23:16:33 +0200 |
store external accesses within name space (as produced by naming policy);
|
file | diff | annotate |
| Mon, 20 Aug 2007 20:44:01 +0200 |
tuned signature;
|
file | diff | annotate |
| Mon, 09 Jul 2007 22:40:57 +0200 |
declare: disallow quote (") in names;
|
file | diff | annotate |
| Thu, 24 May 2007 08:37:37 +0200 |
tuned Pure/General/name_space.ML
|
file | diff | annotate |
| Wed, 10 Jan 2007 20:17:26 +0100 |
removed NameSpace.split -- use qualifier/base instead;
|
file | diff | annotate |
| Sat, 30 Dec 2006 16:08:00 +0100 |
removed conditional combinator;
|
file | diff | annotate |
| Wed, 27 Dec 2006 19:10:05 +0100 |
added split
|
file | diff | annotate |
| Fri, 15 Dec 2006 00:08:06 +0100 |
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 |
renamed NameSpace.drop_base to NameSpace.qualifier;
|
file | diff | annotate |
| Sat, 08 Apr 2006 22:51:22 +0200 |
tuned;
|
file | diff | annotate |
| Tue, 21 Mar 2006 12:18:15 +0100 |
avoid polymorphic equality;
|
file | diff | annotate |
| Wed, 15 Feb 2006 21:35:06 +0100 |
removed qualified_force_prefix;
|
file | diff | annotate |
| Sun, 12 Feb 2006 21:34:24 +0100 |
low-level tuning of merge: maintain identity of accesses;
|
file | diff | annotate |
| Sat, 11 Feb 2006 17:17:50 +0100 |
removed custom_accesses;
|
file | diff | annotate |
| Mon, 06 Feb 2006 20:59:06 +0100 |
tuned;
|
file | diff | annotate |
| Fri, 28 Oct 2005 16:35:40 +0200 |
cleaned up nth, nth_update, nth_map and nth_string functions
|
file | diff | annotate |
| Tue, 04 Oct 2005 19:01:37 +0200 |
minor tweaks for Poplog/ML;
|
file | diff | annotate |
| Thu, 15 Sep 2005 17:16:56 +0200 |
TableFun/Symtab: curried lookup and update;
|
file | diff | annotate |
| Thu, 01 Sep 2005 18:48:50 +0200 |
curried_lookup/update;
|
file | diff | annotate |
| Sun, 28 Aug 2005 16:04:47 +0200 |
removed unused dest operation;
|
file | diff | annotate |
| Thu, 14 Jul 2005 19:28:32 +0200 |
added dest_table;
|
file | diff | annotate |
| Fri, 17 Jun 2005 18:33:29 +0200 |
Symtab.fold;
|
file | diff | annotate |
| Thu, 09 Jun 2005 12:03:28 +0200 |
added type NameSpace.table with basic operations;
|
file | diff | annotate |
| Sun, 05 Jun 2005 11:31:25 +0200 |
no warning for non-identifiers;
|
file | diff | annotate |
| Tue, 31 May 2005 11:53:28 +0200 |
renamed cond_extern to extern;
|
file | diff | annotate |
| Wed, 18 May 2005 11:30:59 +0200 |
tuned;
|
file | diff | annotate |
| Thu, 24 Mar 2005 17:03:37 +0100 |
Further work on interpretation commands. New command `interpret' for
|
file | diff | annotate |
| Fri, 04 Mar 2005 15:07:34 +0100 |
Removed practically all references to Library.foldr.
|
file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 |
Move towards standard functions.
|
file | diff | annotate |
| Sun, 13 Feb 2005 17:15:14 +0100 |
Deleted Library.option type.
|
file | diff | annotate |
| Tue, 06 Jul 2004 20:31:37 +0200 |
added flag unique_names
|
file | diff | annotate |