src/Pure/Isar/token.ML
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2010-12-04 wenzelm 2010-12-04 eliminated obsolete Token.Malformed -- subsumed by Token.Error;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-13 wenzelm 2010-11-13 simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
2010-11-13 wenzelm 2010-11-13 eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-11-13 wenzelm 2010-11-13 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);
2010-10-30 wenzelm 2010-10-30 support for floating-point tokens in outer syntax (coinciding with inner syntax version);
2010-08-07 wenzelm 2010-08-07 more robust treatment of Markup.token;
2010-08-07 wenzelm 2010-08-07 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;