src/Pure/Isar/token.ML
2012-08-23 wenzelm 2012-08-23 tuned messages: end-of-input rarely means physical end-of-file from the past;
2012-08-23 wenzelm 2012-08-23 clarified type Token.file;
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language;
2012-08-11 wenzelm 2012-08-11 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
2012-08-10 wenzelm 2012-08-10 proper error prefixes;
2012-08-09 wenzelm 2012-08-09 some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
2012-08-09 wenzelm 2012-08-09 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
2012-08-09 wenzelm 2012-08-09 tuned signature;
2012-03-04 wenzelm 2012-03-04 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-09-02 wenzelm 2011-09-02 more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-12 wenzelm 2011-07-12 more precise Symbol_Pos.quote_string;
2011-07-10 wenzelm 2011-07-10 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;
2011-07-08 wenzelm 2011-07-08 discontinued special treatment of hard tabulators;
2011-04-30 wenzelm 2011-04-30 more uniform variations of scan_string;
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;