src/Pure/Isar/token.ML
2011-09-02 ago more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-07-23 ago defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-12 ago more precise Symbol_Pos.quote_string;
2011-07-10 ago inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
2011-07-08 ago discontinued special treatment of hard tabulators;
2011-04-30 ago more uniform variations of scan_string;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2010-12-04 ago eliminated obsolete Token.Malformed -- subsumed by Token.Error;
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-13 ago simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
2010-11-13 ago eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-11-13 ago simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
2010-10-30 ago support for floating-point tokens in outer syntax (coinciding with inner syntax version);
2010-08-07 ago more robust treatment of Markup.token;
2010-08-07 ago simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;