src/Pure/ML/ml_lex.ML
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-09-06 wenzelm 2011-09-06 bulk reports for improved message throughput;
2011-09-04 wenzelm 2011-09-04 eliminated markup for plain identifiers (frequent but insignificant); reduced "black" markup (outer string etc. takes care of it already);
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-01-10 wenzelm 2011-01-10 refined ML_Lex.flatten: ensure proper separation of tokens;
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 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-11-04 wenzelm 2010-11-04 warn in correlation with report -- avoid spurious message duplicates;
2010-11-03 wenzelm 2010-11-03 explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-08-18 wenzelm 2010-08-18 uniform Markup.empty/Markup.Empty in ML and Scala;
2010-05-31 wenzelm 2010-05-31 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
2010-05-30 wenzelm 2010-05-30 separate markup for ML delimiters;
2009-06-10 wenzelm 2009-06-10 allow Isabelle symbols within low-level ML source;
2009-06-06 wenzelm 2009-06-06 export end_pos_of;
2009-06-04 wenzelm 2009-06-04 tuned signature;
2009-06-01 wenzelm 2009-06-01 added flatten;
2009-03-24 wenzelm 2009-03-24 datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-22 wenzelm 2009-03-22 added read_antiq, with improved error reporting; tuned signature; tuned;
2009-03-22 wenzelm 2009-03-22 ML_Lex.pos_of: regular position; added ML_Lex.text_of;
2009-03-20 wenzelm 2009-03-20 report markup for ML tokens;
2009-03-20 wenzelm 2009-03-20 allow non-printable symbols within string tokens;
2009-03-19 wenzelm 2009-03-19 added scan_antiq; more robust scan_ml: plain scanning without cut, regular Symbol_Pos.content instead of Symbol_Pos.implode (which contains spurious Symbol.DEL is used with proper positions);
2009-03-19 wenzelm 2009-03-19 added tokenize; internal scan_str: ensure Symbol.is_regular, otherwise it might swallow the stopper and crash!
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-08-09 wenzelm 2008-08-09 renamed ML_Lex.val_of to content_of;
2008-08-09 wenzelm 2008-08-09 tuned SymbolPos interface;
2008-08-07 wenzelm 2008-08-07 improved position handling due to SymbolPos.T; SymbolPos.scan_comment; tuned;
2008-08-04 wenzelm 2008-08-04 abstract type Scan.stopper;
2007-09-16 wenzelm 2007-09-16 removed obsolete Selector token; tuned signature; string syntax: proper escape format;
2007-09-15 wenzelm 2007-09-15 Lexical syntax for SML.