Sat, 18 Jun 2011 11:45:07 +0200 |
wenzelm |
more uniform treatment of "keyword" vs. "operator";
|
file |
diff |
annotate
|
Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
Sun, 09 Jan 2011 20:30:47 +0100 |
wenzelm |
more direct treatment of Position.end_offset;
|
file |
diff |
annotate
|
Sat, 04 Dec 2010 15:14:28 +0100 |
wenzelm |
eliminated obsolete Token.Malformed -- subsumed by Token.Error;
|
file |
diff |
annotate
|
Sat, 13 Nov 2010 20:13:35 +0100 |
wenzelm |
report malformed symbols;
|
file |
diff |
annotate
|
Sat, 13 Nov 2010 19:21:53 +0100 |
wenzelm |
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
|
file |
diff |
annotate
|
Sat, 30 Oct 2010 15:26:40 +0200 |
wenzelm |
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
|
file |
diff |
annotate
|
Mon, 25 Oct 2010 20:24:13 +0200 |
wenzelm |
explicitly qualify type Output.output, which is a slightly odd internal feature;
|
file |
diff |
annotate
|
Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 11:02:47 +0200 |
wenzelm |
uniform Markup.empty/Markup.Empty in ML and Scala;
|
file |
diff |
annotate
|
Tue, 17 Aug 2010 22:57:11 +0200 |
wenzelm |
report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
|
file |
diff |
annotate
|
Sun, 15 Aug 2010 20:19:56 +0200 |
wenzelm |
rename "unit" to "atom", to avoid confusion with the unit type;
|
file |
diff |
annotate
|
Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
Sun, 30 May 2010 18:23:50 +0200 |
wenzelm |
more detailed token markup, including command kind as sub_kind;
|
file |
diff |
annotate
|
Sun, 30 May 2010 14:21:35 +0200 |
wenzelm |
simplified command/keyword markup;
|
file |
diff |
annotate
|
Sun, 30 May 2010 14:14:30 +0200 |
wenzelm |
markup non-identifier keyword as operator;
|
file |
diff |
annotate
|
Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
|
Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
Fri, 02 Jan 2009 19:38:14 +0100 |
wenzelm |
more detailed inner token markup;
|
file |
diff |
annotate
|
Fri, 02 Jan 2009 16:21:47 +0100 |
wenzelm |
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
|
file |
diff |
annotate
| base
|