src/Pure/General/name_space.ML
Fri, 26 Aug 2022 12:38:00 +0200 wenzelm removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
Fri, 12 Nov 2021 13:02:20 +0100 wenzelm clarified properties: avoid empty entry;
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
Tue, 07 Sep 2021 22:35:44 +0200 wenzelm more markup, e.g. to locate defining theory node in formal document output;
Tue, 07 Sep 2021 21:47:50 +0200 wenzelm tuned signature;
Tue, 07 Sep 2021 21:16:22 +0200 wenzelm export other entities, e.g. relevant for formal document output;
Tue, 24 Aug 2021 14:56:55 +0200 wenzelm clarified signature;
Fri, 17 Jul 2020 14:56:55 +0200 wenzelm prefer conservative extend/merge of theory naming;
Fri, 03 Apr 2020 13:51:56 +0200 wenzelm more accurate context position reports;
Mon, 09 Dec 2019 11:17:34 +0100 wenzelm clarified signature: store full theory name;
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature;
Thu, 03 Jan 2019 14:12:44 +0100 wenzelm clarified signature: more types;
Mon, 12 Nov 2018 15:14:12 +0100 wenzelm clarified signature;
Thu, 25 Oct 2018 15:41:40 +0200 wenzelm proper completion for @{named_theorems};
Sun, 13 May 2018 15:05:21 +0200 wenzelm more operations;
Mon, 03 Jul 2017 14:24:55 +0200 wenzelm complete on long name components as well;
Mon, 03 Jul 2017 09:57:26 +0200 wenzelm tuned;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Tue, 18 Oct 2016 17:41:56 +0200 wenzelm replaced inefficient valid_accesses by is_valid_access, based on stored input accesses: e.g. relevant for Proof_Context.update_thms;
Mon, 06 Jun 2016 10:34:56 +0200 wenzelm less redundant exploration of full name space;
Mon, 06 Jun 2016 08:36:03 +0200 wenzelm tuned;
Sun, 17 Apr 2016 20:11:02 +0200 wenzelm clarified signature;
Thu, 14 Apr 2016 23:31:10 +0200 wenzelm highlighting of entity def/ref positions wrt. cursor;
Wed, 13 Apr 2016 16:46:05 +0200 wenzelm more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
Sun, 24 Jan 2016 15:02:56 +0100 wenzelm tuned signature;
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala;
Wed, 13 May 2015 19:12:59 +0200 wenzelm clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
Wed, 13 May 2015 17:27:12 +0200 wenzelm more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;
Thu, 09 Apr 2015 20:42:32 +0200 wenzelm clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
Mon, 06 Apr 2015 22:11:01 +0200 wenzelm support for 'restricted' modifier: only qualified accesses outside the local scope;
Sat, 04 Apr 2015 21:30:58 +0200 wenzelm tuned message;
Sat, 04 Apr 2015 14:04:11 +0200 wenzelm support private scope for individual local theory commands;
Fri, 03 Apr 2015 19:56:51 +0200 wenzelm more uniform "verbose" option to print name space;
Thu, 02 Apr 2015 20:07:05 +0200 wenzelm export for informative purposes;
Wed, 01 Apr 2015 11:55:23 +0200 wenzelm tuned message;
Wed, 01 Apr 2015 10:35:43 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 23:42:57 +0200 wenzelm more visibility flags on background naming;
Tue, 31 Mar 2015 22:31:05 +0200 wenzelm support for explicit scope of private entries;
Tue, 31 Mar 2015 21:12:22 +0200 wenzelm subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
Tue, 31 Mar 2015 20:18:10 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 20:07:37 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 19:16:44 +0200 wenzelm tuned;
Tue, 31 Mar 2015 11:16:55 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 00:11:54 +0200 wenzelm tuned signature;
Mon, 30 Mar 2015 22:34:59 +0200 wenzelm support for strictly private name space entries;
Wed, 25 Mar 2015 14:39:40 +0100 wenzelm semantic completion for @{system_option};
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Mon, 13 Oct 2014 22:43:29 +0200 wenzelm tuned signature;
Mon, 11 Aug 2014 20:30:01 +0200 wenzelm clarified signature: entity serial number is not position id;
Sun, 06 Apr 2014 16:36:28 +0200 wenzelm more source positions;
Mon, 17 Mar 2014 10:01:58 +0100 wenzelm more uniform alias vs. hide: proper check, allow to hide global names as well;
Sat, 15 Mar 2014 15:50:41 +0100 wenzelm minor tuning;
Sat, 15 Mar 2014 12:51:14 +0100 wenzelm clarified completion ordering: prefer local names;
Sat, 15 Mar 2014 11:57:55 +0100 wenzelm tuned -- avoid vacuous reports;
Thu, 13 Mar 2014 17:26:22 +0100 wenzelm more frugal recording of changes: join merely requires information from one side;
Tue, 11 Mar 2014 22:49:28 +0100 wenzelm more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
Tue, 11 Mar 2014 14:28:39 +0100 wenzelm tuned signature;
Mon, 10 Mar 2014 22:14:53 +0100 wenzelm tuned messages -- in accordance to Isabelle/Scala;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Mon, 10 Mar 2014 10:13:47 +0100 wenzelm more structured order;
less more (0) -100 -60 tip