src/Pure/ML/ml_lex.ML
2016-04-01 wenzelm 2016-04-01 tuned signature;
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2015-11-07 wenzelm 2015-11-07 ML cartouches via control antiquotation;
2015-10-20 wenzelm 2015-10-20 another antiquotation short form: undecorated cartouche as alias for @{text}; document antiquotation @{text} ignores option "source";
2015-10-19 wenzelm 2015-10-19 tuned;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-10-18 wenzelm 2015-10-18 support control symbol antiquotations;
2015-10-16 wenzelm 2015-10-16 clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
2014-12-10 wenzelm 2014-12-10 tuned;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-12-08 wenzelm 2014-12-08 some special cases for official SML, to treat Isabelle symbols like raw characters;
2014-12-08 wenzelm 2014-12-08 tuned comment;
2014-12-03 wenzelm 2014-12-03 tuned;
2014-11-30 wenzelm 2014-11-30 tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-07 wenzelm 2014-11-07 tuned markup;
2014-11-01 wenzelm 2014-11-01 recover via scanner; tuned signature;
2014-11-01 wenzelm 2014-11-01 simplified -- scanning is never interactive;
2014-10-31 wenzelm 2014-10-31 removed pointless markup; tuned comments;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete \<^sync> marker;
2014-04-08 wenzelm 2014-04-08 no report for position singularity, notably for aux. file, especially empty one;
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-19 wenzelm 2014-02-19 tuned signature;
2014-02-18 wenzelm 2014-02-18 generic markup for embedded languages;
2014-02-15 wenzelm 2014-02-15 more uniform ML keyword markup; tuned;
2014-02-14 wenzelm 2014-02-14 tuned;
2014-01-20 wenzelm 2014-01-20 tuned -- more direct err_prefix;
2014-01-20 wenzelm 2014-01-20 tuned errors;
2013-08-23 wenzelm 2013-08-23 discontinued unused antiquotation blocks;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-11 wenzelm 2012-08-11 clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
2012-08-10 wenzelm 2012-08-10 sneak message into "bad" markup as property -- to be displayed after YXML parsing;
2012-08-10 wenzelm 2012-08-10 more visible markup of malformed input as "bad";
2012-08-09 wenzelm 2012-08-09 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
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;