src/Pure/Isar/token.scala
2014-02-14 wenzelm 2014-02-14 tuned signature (in accordance to ML version);
2014-02-14 wenzelm 2014-02-14 tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
2014-01-25 wenzelm 2014-01-25 semicolon is minor keyword (see also 29f1e53f9937);
2014-01-18 wenzelm 2014-01-18 unused;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-01-25 wenzelm 2013-01-25 clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally; reverted f3588e59aeaa accordingly;
2012-08-10 wenzelm 2012-08-10 clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;
2012-08-07 wenzelm 2012-08-07 more structural parsing for minor modes; tuned signatures;
2012-07-30 wenzelm 2012-07-30 allow negative int values as well, according to real = int | float;
2012-07-30 wenzelm 2012-07-30 tuned signature;
2012-07-20 wenzelm 2012-07-20 basic support for stand-alone options with external string representation;
2012-07-19 wenzelm 2012-07-19 support Session.Queue with ordering and dependencies;
2012-07-18 wenzelm 2012-07-18 more informative errors;
2012-03-19 wenzelm 2012-03-19 clarified command span classification: strict Command.is_command, permissive Command.name;
2012-03-15 wenzelm 2012-03-15 clarified syntax of prospective keywords;
2011-06-30 wenzelm 2011-06-30 more general theory header parsing;
2011-06-18 wenzelm 2011-06-18 more uniform treatment of "keyword" vs. "operator";
2011-06-17 wenzelm 2011-06-17 recovered markup for non-alphabetic keywords;
2010-10-30 wenzelm 2010-10-30 support for floating-point tokens in outer syntax (coinciding with inner syntax version);
2010-08-12 wenzelm 2010-08-12 more basic notion of unparsed input;
2010-05-17 wenzelm 2010-05-17 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;