src/Pure/General/scan.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-18 wenzelm 2014-01-18 tuned;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-08-13 wenzelm 2013-08-13 discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end; document antiquotations: renamed term style "isub" to "sub";
2013-08-08 wenzelm 2013-08-08 more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
2013-07-10 wenzelm 2013-07-10 more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
2012-08-23 wenzelm 2012-08-23 eliminated obsolete byte_reader -- theory headers + body files are parsed in full;
2012-08-10 wenzelm 2012-08-10 more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
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-09 wenzelm 2012-08-09 tuned;
2012-08-09 wenzelm 2012-08-09 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
2012-07-20 wenzelm 2012-07-20 more explicit java.io.{File => JFile};
2012-07-18 wenzelm 2012-07-18 tuned import;
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-02-23 wenzelm 2012-02-23 avoid trait Addable, which is deprecated in scala-2.9.x; tuned;
2011-12-16 wenzelm 2011-12-16 prefer sorting from Scala library;
2011-10-22 wenzelm 2011-10-22 class Lexicon as abstract datatype;
2011-07-07 wenzelm 2011-07-07 explicit indication of type Symbol.Symbol;
2011-07-07 wenzelm 2011-07-07 simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages;
2011-06-17 wenzelm 2011-06-17 unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);
2011-06-16 wenzelm 2011-06-16 partial scans of nested comments;
2011-06-16 wenzelm 2011-06-16 some support for partial scans with explicit context; clarified junk vs. junk1;
2011-05-12 wenzelm 2011-05-12 minor adaption for scala-2.9.0.final;
2011-04-21 wenzelm 2011-04-21 more robust scanning of iterated comments, such as "(* (**) (**) *)";
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-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;
2010-05-05 wenzelm 2010-05-05 use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;
2010-03-29 wenzelm 2010-03-29 replaced some deprecated methods;
2010-03-29 wenzelm 2010-03-29 adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
2010-01-11 wenzelm 2010-01-11 clarified Symbol.is_plain/is_wellformed -- is_closed was rejecting plain backslashes;
2010-01-10 wenzelm 2010-01-10 tuned;
2010-01-05 wenzelm 2010-01-05 more accurate scanning of bad input;
2010-01-05 wenzelm 2010-01-05 tuned;
2009-12-27 wenzelm 2009-12-27 quoted_content: handle escapes;
2009-12-27 wenzelm 2009-12-27 added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
2009-12-22 wenzelm 2009-12-22 explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure; added Token_Reader; tuned;
2009-12-20 wenzelm 2009-12-20 improve performance by reordering of parser combinators;
2009-12-20 wenzelm 2009-12-20 added nested comments; tuned;
2009-12-20 wenzelm 2009-12-20 simplified result of keyword and symbols parser; some support for parsing outer syntax tokens;
2009-12-19 wenzelm 2009-12-19 refined some Symbol operations/signatures; added Symbol.Matcher; flexible Scan.Lexicon.symbols, with one/many/many1 variants;
2009-12-19 wenzelm 2009-12-19 indicate final state of keywords; added symbol scanner;
2009-08-29 wenzelm 2009-08-29 misc tuning;
2009-06-23 wenzelm 2009-06-23 moved string utilities to completion.scala; tuned;
2009-06-23 wenzelm 2009-06-23 more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++; misc tuning;
2009-06-22 wenzelm 2009-06-22 Lexicon: removed unused max_entry;
2009-06-18 wenzelm 2009-06-18 subSequence: bounds checking;
2009-06-18 wenzelm 2009-06-18 added reverse CharSequence;
2009-06-16 wenzelm 2009-06-16 added completions; misc simplification via aux. operations;
2009-06-16 wenzelm 2009-06-16 reorganized and abstracted version, via Set trait;
2009-06-16 wenzelm 2009-06-16 Efficient scanning of literals.