clarified modules;
more operations;

support for formal comments in ML in Isabelle/Scala;

tuned;

separate JSON lexer;

more robust treatment of UTF8 in raw byte sources;

tuned signature;

support 'abbrevs' within theory header;
simplified 'keywords': no abbreviations here;

tuned;

more merge operations;

misc tuning, based on warnings by IntelliJ IDEA;

actually finish after closing, e.g. relevant for consecutive (**)(**);

avoid deprecated Scala syntax;

support URLs as well;

reclaimed Byte_Reader from 51560e392e1b;

avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;

tuned;

tuned signature -- emphasize line-oriented aspect;

partial scans via ML_Lex.tokenize_context;
simplified ML_char: no gaps (hardly relevant in practice);
tuned;

lexical syntax for SML (in Scala);
tuned;

tuned signature (in accordance to ML version);

tuned signature -- separate Lexicon from Parsers (in accordance to ML version);

tuned;

support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;

discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
document antiquotations: renamed term style "isub" to "sub";

more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;

more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;

eliminated obsolete byte_reader -- theory headers + body files are parsed in full;

more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;

clarified undefined, unparsed, unfinished command spans;
common reparse_spans, diff_commands;
some support for consolidate_spans after change of perspective;

tuned;

refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;

more explicit java.io.{File => JFile};

tuned import;

prefer final ADTs -- prevent ooddities;

avoid trait Addable, which is deprecated in scala-2.9.x;
tuned;

prefer sorting from Scala library;

class Lexicon as abstract datatype;

explicit indication of type Symbol.Symbol;

simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
tuned implicit build/init messages;

unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);

partial scans of nested comments;

some support for partial scans with explicit context;
clarified junk vs. junk1;

minor adaption for scala-2.9.0.final;

more robust scanning of iterated comments, such as "(* (**) (**) *)";

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);

support for floating-point tokens in outer syntax (coinciding with inner syntax version);

more basic notion of unparsed input;

renamed class Outer_Lex to Token and Token_Kind to Token.Kind;

--HG--
rename : src/Pure/Isar/outer_lex.scala => src/Pure/Isar/token.scala

use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;

replaced some deprecated methods;

adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;

clarified Symbol.is_plain/is_wellformed -- is_closed was rejecting plain backslashes;

tuned;

more accurate scanning of bad input;

tuned;

quoted_content: handle escapes;

added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);

explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
added Token_Reader;
tuned;

improve performance by reordering of parser combinators;

added nested comments;
tuned;

simplified result of keyword and symbols parser;
some support for parsing outer syntax tokens;

refined some Symbol operations/signatures;
added Symbol.Matcher;
flexible Scan.Lexicon.symbols, with one/many/many1 variants;

indicate final state of keywords;
added symbol scanner;

misc tuning;

moved string utilities to completion.scala;
tuned;

more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
misc tuning;

Lexicon: removed unused max_entry;

subSequence: bounds checking;

added reverse CharSequence;

added completions;
misc simplification via aux. operations;

reorganized and abstracted version, via Set trait;

Efficient scanning of literals.