src/Pure/General/completion.scala
20 months ago wenzelm 2017-11-01 tuned;
20 months ago wenzelm 2017-11-01 init only once (see also c0f776b661fa);
20 months ago wenzelm 2017-10-05 completion supports theory header imports; tuned;
20 months ago wenzelm 2017-10-05 tuned signature;
2017-06-21 wenzelm 2017-06-21 tuned signature;
2017-06-21 wenzelm 2017-06-21 tuned signature;
2017-06-09 wenzelm 2017-06-09 clarified output for symbol completion;
2017-06-09 wenzelm 2017-06-09 tuned;
2017-04-01 wenzelm 2017-04-01 clarified YXML vs. symbol encoding: operate on whole message;
2016-09-16 wenzelm 2016-09-16 more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
2016-09-14 wenzelm 2016-09-14 clarified GUI representation of replacement texts with zero or more abbrevs;
2016-09-14 wenzelm 2016-09-14 discontinued global etc/abbrevs;
2016-09-14 wenzelm 2016-09-14 tuned;
2016-09-06 wenzelm 2016-09-06 strictly sequential abbrevs;
2016-09-01 wenzelm 2016-09-01 more careful quoting, e.g. relevant for \<^control>cartouche;
2016-08-02 wenzelm 2016-08-02 implicit keyword completion only for actual words (amending 73939a9b70a3);
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-08-02 wenzelm 2016-08-02 tuned;
2016-05-24 wenzelm 2016-05-24 cartouche abbreviations work both for " as well;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-04-13 wenzelm 2016-04-13 avoid quotes for qualified names;
2016-01-23 wenzelm 2016-01-23 empty abbrevs are removed globally;
2015-12-29 wenzelm 2015-12-29 support additional abbrevs;
2015-11-10 wenzelm 2015-11-10 smart quoting of non-identifiers, e.g. jEdit actions;
2015-11-10 wenzelm 2015-11-10 allow open symboloid;
2015-11-07 wenzelm 2015-11-07 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-07 wenzelm 2015-11-07 tuned;
2015-09-03 wenzelm 2015-09-03 clean name as in ML Completion.make;
2015-07-16 wenzelm 2015-07-16 clarified boundary cases of completion;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-03-16 wenzelm 2015-03-16 support for completion reports produced in Scala (inlined into messages);
2015-01-08 wenzelm 2015-01-08 tuned;
2014-12-01 wenzelm 2014-12-01 more merge operations;
2014-07-22 wenzelm 2014-07-22 no keyword completion within word context -- especially avoid its odd visual rendering;
2014-07-21 wenzelm 2014-07-21 always complete explicit symbols;
2014-07-21 wenzelm 2014-07-21 discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
2014-05-06 wenzelm 2014-05-06 hardwired default_frequency to avoid fluctuation of popup content;
2014-04-30 wenzelm 2014-04-30 support for long names in Scala;
2014-04-29 wenzelm 2014-04-29 more systematic Isabelle output, like in classic Isabelle/ML (without markup);
2014-04-22 wenzelm 2014-04-22 avoid octal escape literals -- deprecated in scala-2.11.0;
2014-04-16 wenzelm 2014-04-16 more specific support for sequence of words;
2014-04-16 wenzelm 2014-04-16 tuned signature -- separate module Word;
2014-04-15 wenzelm 2014-04-15 clarified abbreviations for cartouche delimiters, to work in any context;
2014-04-13 wenzelm 2014-04-13 added spell-checker completion dialog, without counting frequency of items due to empty name; tuned signature;
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-19 wenzelm 2014-03-19 accomodate word as part of schematic variable name;
2014-03-17 wenzelm 2014-03-17 merge semantic and syntax completion; tuned;
2014-03-17 wenzelm 2014-03-17 tuned;
2014-03-17 wenzelm 2014-03-17 tuned signature;
2014-03-15 wenzelm 2014-03-15 clarified completion ordering: prefer local names;
2014-03-10 wenzelm 2014-03-10 proper Char comparison, despite weakly-typed Scala (cf. 5ff5208de089);
2014-03-10 wenzelm 2014-03-10 include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');
2014-03-09 wenzelm 2014-03-09 do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
2014-03-08 wenzelm 2014-03-08 allow suffix of underscores for words (notably keywords), similar to semantic completion;
2014-03-08 wenzelm 2014-03-08 no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;
2014-03-08 wenzelm 2014-03-08 clarified description; tuned;
2014-03-08 wenzelm 2014-03-08 tuned;
2014-03-07 wenzelm 2014-03-07 more strict discrimination: symbols vs. keywords could overlap;
2014-03-07 wenzelm 2014-03-07 tuned;
2014-03-07 wenzelm 2014-03-07 more accurate description;