| 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
|
| Tue, 31 Mar 2015 22:31:05 +0200 |
wenzelm |
support for explicit scope of private entries;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 20:18:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 20:07:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 19:16:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 11:16:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|