| Wed, 03 May 2023 23:11:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 May 2023 11:34:47 +0200 |
wenzelm |
proper treatment of restriction (for 'qualified');
|
file |
diff |
annotate
|
| Tue, 02 May 2023 23:22:30 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 22:33:07 +0200 |
wenzelm |
more complete accesses for hide operation (amending fcd85e04a948), e.g. relevant for AFP/thys/Jordan_Normal_Form/Matrix_Kernel.thy in AFP/4d8afd37b465;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 14:19:34 +0200 |
wenzelm |
minor performance tuning: more compact representation of only sparsely table;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 11:38:53 +0200 |
wenzelm |
minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 11:11:19 +0200 |
wenzelm |
proper checks;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 10:49:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 10:32:04 +0200 |
wenzelm |
tuned structure;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 10:13:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 01 May 2023 22:47:51 +0200 |
wenzelm |
clarified extern vs. alias/hide: output alternative names, if possible;
|
file |
diff |
annotate
|
| Mon, 01 May 2023 22:19:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 26 Apr 2023 15:38:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 22:26:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 13:52:06 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 16:01:00 +0200 |
wenzelm |
proforma use of Long_Name.chunks, without change of the representation of accesses yet;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2023 23:08:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2023 15:22:52 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2023 12:57:10 +0200 |
wenzelm |
more compact: avoid redundant entries;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2023 11:27:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2023 11:25:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 11:16:33 +0200 |
wenzelm |
minor performance tuning: more compact persistent data;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 09:54:46 +0200 |
wenzelm |
unused (see 34dd96a06c45);
|
file |
diff |
annotate
|
| 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();
|
file |
diff |
annotate
|
| Fri, 12 Nov 2021 13:02:20 +0100 |
wenzelm |
clarified properties: avoid empty entry;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 22:35:44 +0200 |
wenzelm |
more markup, e.g. to locate defining theory node in formal document output;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 21:47:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 21:16:22 +0200 |
wenzelm |
export other entities, e.g. relevant for formal document output;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2021 14:56:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 14:56:55 +0200 |
wenzelm |
prefer conservative extend/merge of theory naming;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 13:51:56 +0200 |
wenzelm |
more accurate context position reports;
|
file |
diff |
annotate
|
| Mon, 09 Dec 2019 11:17:34 +0100 |
wenzelm |
clarified signature: store full theory name;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Mon, 12 Nov 2018 15:14:12 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 15:41:40 +0200 |
wenzelm |
proper completion for @{named_theorems};
|
file |
diff |
annotate
|
| Sun, 13 May 2018 15:05:21 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 14:24:55 +0200 |
wenzelm |
complete on long name components as well;
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 09:57:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 10:34:56 +0200 |
wenzelm |
less redundant exploration of full name space;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 08:36:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 20:11:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 23:31:10 +0200 |
wenzelm |
highlighting of entity def/ref positions wrt. cursor;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 16:46:05 +0200 |
wenzelm |
more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 15:02:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| 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";
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 21:30:58 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 14:04:11 +0200 |
wenzelm |
support private scope for individual local theory commands;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Thu, 02 Apr 2015 20:07:05 +0200 |
wenzelm |
export for informative purposes;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 11:55:23 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 10:35:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 23:42:57 +0200 |
wenzelm |
more visibility flags on background naming;
|
file |
diff |
annotate
|