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