src/Pure/General/name_space.ML
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;
Mon, 10 Mar 2014 09:54:01 +0100 wenzelm more restrictive completion: intern/extern stability;
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 "__");
Fri, 07 Mar 2014 14:37:25 +0100 wenzelm more detailed description of completion items;
Fri, 07 Mar 2014 11:48:11 +0100 wenzelm no completion of concealed names;
Thu, 06 Mar 2014 21:32:09 +0100 wenzelm special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
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;
Thu, 06 Mar 2014 16:24:47 +0100 wenzelm more compact Markup.markup_report: message body may consist of multiple elements;
Thu, 06 Mar 2014 16:12:26 +0100 wenzelm reject internal term names outright, and complete consts instead;
Wed, 05 Mar 2014 19:52:28 +0100 wenzelm tuned;
Wed, 05 Mar 2014 18:26:35 +0100 wenzelm more markup for inner syntax class/type names (notably for completion);
Sun, 02 Mar 2014 22:03:27 +0100 wenzelm allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
Sun, 02 Mar 2014 20:34:11 +0100 wenzelm consider completion report as part of error message -- less stateful, may get handled;
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;
Sun, 23 Feb 2014 21:30:47 +0100 wenzelm tuned whitespace;
Sun, 23 Feb 2014 21:11:59 +0100 wenzelm clarified semantic completion: retain kind.full_name as official item name for history;
Sun, 23 Feb 2014 14:39:51 +0100 wenzelm clarified completion names;
Sat, 22 Feb 2014 20:52:43 +0100 wenzelm support for completion within the formal context;
Sat, 22 Feb 2014 16:58:02 +0100 wenzelm tuned signature;
Wed, 11 Sep 2013 15:42:05 +0200 wenzelm tuned signature;
Sun, 12 May 2013 20:25:45 +0200 wenzelm some system options as context-sensitive config options;
Mon, 25 Mar 2013 13:37:44 +0100 wenzelm tuned print_classes: more standard order, markup, formatting;
Fri, 30 Nov 2012 22:38:06 +0100 wenzelm print formal entities with markup;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 11 Oct 2012 12:38:18 +0200 wenzelm more position information for hyperlink and placement of message;
Sat, 22 Sep 2012 19:32:30 +0200 wenzelm report proper binding positions only -- avoid swamping document model with unspecific information;
Fri, 14 Sep 2012 18:12:41 +0200 wenzelm clarified markup names;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
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);
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Sun, 18 Mar 2012 10:28:31 +0100 wenzelm tuned structure;
Sun, 11 Mar 2012 14:09:01 +0100 wenzelm more direct Name_Space.defined_entry;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Tue, 08 Nov 2011 21:09:35 +0100 wenzelm entity markup for bound variables;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Tue, 03 May 2011 22:27:32 +0200 wenzelm more conventional naming scheme: names_long, names_short, names_unique;
Wed, 27 Apr 2011 20:37:56 +0200 wenzelm more informative markup for fixed variables (via name space entry);
less more (0) -100 -60 tip