2012-11-27 ago support for sub-structured identifier syntax (inactive);
2012-11-26 ago tuned signature;
2012-11-26 ago more uniform Symbol.is_ascii_identifier in ML/Scala;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-11 ago clarified output token markup (see also bc22daeed49e);
2012-08-29 ago renamed Position.str_of to;
2012-02-15 ago renamed "xstr" to "str_token";
2011-12-01 ago renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
2011-11-28 ago separate module for concrete Isabelle markup;
2011-09-06 ago bulk reports for improved message throughput;
2011-09-04 ago eliminated markup for plain identifiers (frequent but insignificant);
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-06-18 ago inner literal/delimiter corresponds to outer keyword/operator;
2011-04-26 ago clarified auxiliary structure Lexicon.Syntax;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-04-06 ago separate structure Term_Position;
2011-03-22 ago update_name_tr: more precise handling of explicit constraints, including positions;
2011-03-22 ago support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
2011-03-21 ago added Lexicon.encode_position, Lexicon.decode_position;
2010-11-13 ago eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-10-30 ago support for floating-point tokens in outer syntax (coinciding with inner syntax version);
2010-09-17 ago Syntax.read_asts error: report token ranges within message -- no side-effect here;
2010-09-17 ago tuned signature of (Context_) variants;
2010-09-07 ago report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
2010-08-18 ago uniform Markup.empty/Markup.Empty in ML and Scala;
2010-08-08 ago prefer where a proper context is available -- notably for "inner" entities;
2010-03-03 ago more systematic mark/unmark operations;
2010-02-21 ago slightly more abstract syntax mark/unmark operations;
2009-03-18 ago de-camelized Symbol_Pos;
2009-01-19 ago removed Ids;
2009-01-02 ago added numeral, which supercedes num, xnum, float;
2008-12-23 ago renamed terminal category "float" to "float_token", to avoid name
2008-11-29 ago New lexical item "float".
2008-09-29 ago report_token/parse_token: back to context-less version;
2008-09-29 ago;
2008-08-15 ago token_kind: add Space, Comment;
2008-08-09 ago pos_of_token: Position.T;
2008-08-09 ago datatype token: maintain range, tuned representation;
2008-08-07 ago improved position handling due to SymbolPos.T;
2008-06-10 ago removed obsolete read_idents;
2008-01-28 ago basic scanners: produce symbol list instead of imploded string;
2007-09-18 ago simplified type int (eliminated, integer);
2007-09-15 ago replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
2007-08-13 ago Lexicon.tokenize: do not appen EndToken yet;
2007-07-12 ago sys_error;
2007-07-11 ago Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-04-14 ago removed redundant string_of_vname (see term.ML);
2007-04-03 ago avoid overloaded integer constants (accomodate Alice);
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-12 ago read_xnum: return leading_zeros, radix;
2006-12-11 ago xstr: disallow backslashes;
2006-09-21 ago member (op =);
2006-08-02 ago renamed Syntax.indexname to Syntax.read_indexname;
2006-07-19 ago export is_tid;
2006-07-11 ago uniform treatment of num/xnum;
2006-07-11 ago tuned;
2006-07-11 ago hex and binary numerals (contributed by Rafal Kolanski)
2006-06-17 ago moved internal/skolem to term.ML;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-03-21 ago avoid polymorphic equality;