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
|
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
|
Mon, 30 Mar 2015 22:34:59 +0200 |
wenzelm |
support for strictly private name space entries;
|
file |
diff |
annotate
|
Wed, 25 Mar 2015 14:39:40 +0100 |
wenzelm |
semantic completion for @{system_option};
|
file |
diff |
annotate
|
Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
Mon, 13 Oct 2014 22:43:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 11 Aug 2014 20:30:01 +0200 |
wenzelm |
clarified signature: entity serial number is not position id;
|
file |
diff |
annotate
|
Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
Mon, 17 Mar 2014 10:01:58 +0100 |
wenzelm |
more uniform alias vs. hide: proper check, allow to hide global names as well;
|
file |
diff |
annotate
|
Sat, 15 Mar 2014 15:50:41 +0100 |
wenzelm |
minor tuning;
|
file |
diff |
annotate
|
Sat, 15 Mar 2014 12:51:14 +0100 |
wenzelm |
clarified completion ordering: prefer local names;
|
file |
diff |
annotate
|
Sat, 15 Mar 2014 11:57:55 +0100 |
wenzelm |
tuned -- avoid vacuous reports;
|
file |
diff |
annotate
|
Thu, 13 Mar 2014 17:26:22 +0100 |
wenzelm |
more frugal recording of changes: join merely requires information from one side;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 11 Mar 2014 14:28:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 10 Mar 2014 22:14:53 +0100 |
wenzelm |
tuned messages -- in accordance to Isabelle/Scala;
|
file |
diff |
annotate
|
Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
Mon, 10 Mar 2014 10:13:47 +0100 |
wenzelm |
more structured order;
|
file |
diff |
annotate
|
Mon, 10 Mar 2014 09:54:01 +0100 |
wenzelm |
more restrictive completion: intern/extern stability;
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 22:19:52 +0100 |
wenzelm |
ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 14:37:25 +0100 |
wenzelm |
more detailed description of completion items;
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 11:48:11 +0100 |
wenzelm |
no completion of concealed names;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 21:32:09 +0100 |
wenzelm |
special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 20:26:43 +0100 |
wenzelm |
completion is part of error (not report) and thus not subject to context visibility -- e.g. relevant for 'fixes' in long statements;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 16:24:47 +0100 |
wenzelm |
more compact Markup.markup_report: message body may consist of multiple elements;
|
file |
diff |
annotate
|
Thu, 06 Mar 2014 16:12:26 +0100 |
wenzelm |
reject internal term names outright, and complete consts instead;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 19:52:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 18:26:35 +0100 |
wenzelm |
more markup for inner syntax class/type names (notably for completion);
|
file |
diff |
annotate
|
Sun, 02 Mar 2014 22:03:27 +0100 |
wenzelm |
allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
|
file |
diff |
annotate
|
Sun, 02 Mar 2014 20:34:11 +0100 |
wenzelm |
consider completion report as part of error message -- less stateful, may get handled;
|
file |
diff |
annotate
|
Tue, 25 Feb 2014 14:34:18 +0100 |
wenzelm |
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
|
file |
diff |
annotate
|
Sun, 23 Feb 2014 21:30:47 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
Sun, 23 Feb 2014 21:11:59 +0100 |
wenzelm |
clarified semantic completion: retain kind.full_name as official item name for history;
|
file |
diff |
annotate
|
Sun, 23 Feb 2014 14:39:51 +0100 |
wenzelm |
clarified completion names;
|
file |
diff |
annotate
|
Sat, 22 Feb 2014 20:52:43 +0100 |
wenzelm |
support for completion within the formal context;
|
file |
diff |
annotate
|
Sat, 22 Feb 2014 16:58:02 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 11 Sep 2013 15:42:05 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 12 May 2013 20:25:45 +0200 |
wenzelm |
some system options as context-sensitive config options;
|
file |
diff |
annotate
|
Mon, 25 Mar 2013 13:37:44 +0100 |
wenzelm |
tuned print_classes: more standard order, markup, formatting;
|
file |
diff |
annotate
|
Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
Thu, 11 Oct 2012 12:38:18 +0200 |
wenzelm |
more position information for hyperlink and placement of message;
|
file |
diff |
annotate
|
Sat, 22 Sep 2012 19:32:30 +0200 |
wenzelm |
report proper binding positions only -- avoid swamping document model with unspecific information;
|
file |
diff |
annotate
|
Fri, 14 Sep 2012 18:12:41 +0200 |
wenzelm |
clarified markup names;
|
file |
diff |
annotate
|
Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
Mon, 19 Mar 2012 20:32:57 +0100 |
wenzelm |
clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
|
file |
diff |
annotate
|
Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
Sun, 18 Mar 2012 10:28:31 +0100 |
wenzelm |
tuned structure;
|
file |
diff |
annotate
|
Sun, 11 Mar 2012 14:09:01 +0100 |
wenzelm |
more direct Name_Space.defined_entry;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Tue, 08 Nov 2011 21:09:35 +0100 |
wenzelm |
entity markup for bound variables;
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
Tue, 03 May 2011 22:27:32 +0200 |
wenzelm |
more conventional naming scheme: names_long, names_short, names_unique;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 20:37:56 +0200 |
wenzelm |
more informative markup for fixed variables (via name space entry);
|
file |
diff |
annotate
|
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
|