src/Pure/General/name_space.ML
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;
less more (0) -100 -15 tip