| 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
|