| 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
|
| Sun, 12 May 2013 20:25:45 +0200 |
wenzelm |
some system options as context-sensitive config options;
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 13:37:44 +0100 |
wenzelm |
tuned print_classes: more standard order, markup, formatting;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 12:38:18 +0200 |
wenzelm |
more position information for hyperlink and placement of message;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 19:32:30 +0200 |
wenzelm |
report proper binding positions only -- avoid swamping document model with unspecific information;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 18:12:41 +0200 |
wenzelm |
clarified markup names;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|