src/Pure/General/name_space.ML
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);
Wed, 27 Apr 2011 17:44:06 +0200 wenzelm export Name_Space.entry_ord;
Sat, 23 Apr 2011 17:02:12 +0200 wenzelm added Name_Space.check/get convenience;
Sun, 17 Apr 2011 21:04:22 +0200 wenzelm tuned signature;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
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;
Mon, 11 Apr 2011 17:11:03 +0200 wenzelm Name_Space.entry_markup: keep def position as separate properties;
Sun, 27 Mar 2011 20:55:01 +0200 wenzelm decode_term: some context-sensitive markup;
Fri, 17 Dec 2010 22:23:56 +0100 wenzelm extra checking of name bindings for classes, types, consts;
Tue, 09 Mar 2010 23:27:35 +0100 wenzelm added Name_Space.alias -- additional accesses for an existing entry;
Wed, 03 Mar 2010 00:33:33 +0100 wenzelm removed unused external_names;
Thu, 18 Feb 2010 20:46:46 +0100 wenzelm more systematic treatment of qualified names derived from binding;
Tue, 17 Nov 2009 14:50:55 +0100 wenzelm uniform new_group/reset_group;
Wed, 28 Oct 2009 17:36:34 +0100 wenzelm let naming transform binding beforehand -- covering only the "conceal" flag for now;
Sun, 25 Oct 2009 19:14:46 +0100 wenzelm Name_Space.naming: maintain group and theory_name as well;
Sun, 25 Oct 2009 12:27:21 +0100 wenzelm allow name space entries to be "concealed" -- via binding/naming/local_theory;
Sat, 24 Oct 2009 21:30:33 +0200 wenzelm maintain position of formal entities via name space;
Sat, 24 Oct 2009 20:54:08 +0200 wenzelm maintain explicit name space kind;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 24 Oct 2009 19:04:57 +0200 wenzelm maintain abstract entry, with position, identity etc.;
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 14 Mar 2009 00:13:50 +0100 wenzelm removed obsolete no_base_names naming policy;
Thu, 12 Mar 2009 13:18:42 +0100 wenzelm renamed sticky_prefix to mandatory_path;
Thu, 12 Mar 2009 11:09:26 +0100 wenzelm renamed bind to define;
less more (0) -100 -60 tip