src/Pure/ML/ml_context.ML
2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-20 ago tuned error, according to "use" in General/secure.ML;
2014-03-18 ago clarified modules;
2014-03-18 ago clarified bootstrap process: switch to ML with context and antiquotations earlier;
2014-03-18 ago tuned signature;
2014-03-18 ago tuned signature -- rearranged modules;
2014-03-12 ago ML_Context.check_antiquotation still required;
2014-03-12 ago simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
2014-03-10 ago clarified Args.check_src: retain name space information for error output;
2014-03-10 ago clarified Args.src: more abstract type, position refers to name only;
2014-03-01 ago clarified language markup: added "delimited" property;
2014-02-25 ago proper context for global data;
2014-02-17 ago more markup;
2013-08-23 ago added Theory.setup convenience;
2013-08-23 ago clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
2013-08-23 ago discontinued unused antiquotation blocks;
2013-08-16 ago more markup via Name_Space.check;
2013-07-15 ago retain compile-time context visibility, which is particularly important for "apply tactic";
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-29 ago renamed Position.str_of to Position.here;
2012-08-12 ago more static antiquotations;
2012-08-11 ago faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2011-11-28 ago separate module for concrete Isabelle markup;
2011-07-08 ago clarified Thy_Load.digest_file -- read ML files only once;
2011-06-27 ago proper checking of @{ML_antiquotation};
2011-06-27 ago ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-04-16 ago modernized structure Proof_Context;
2011-01-09 ago ML_trace: observe context visibility flag (import for Latex mode, for example);
2010-12-21 ago configuration option "ML_trace";
2010-10-01 ago moved ML_Context.value to Code_Runtime
2010-09-30 ago value uses bare compiler invocation: generated code does not contain antiquotations
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 ago tuned signature of (Context_)Position.report variants;
2010-09-15 ago replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
2010-09-06 ago ML_Context.thm and ML_Context.thms no longer pervasive;
2010-09-06 ago ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
2010-08-31 ago evaluate takes ml context and ml expression parameter
2010-08-25 ago ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
2010-08-08 ago prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
2010-05-30 ago replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-02-07 ago simplified interface for ML antiquotations, struct_name is always "Isabelle";
2009-10-27 ago critical comments;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-06-01 ago structure ML_Compiler;
2009-06-01 ago moved local ML environment to separate module ML_Env;
2009-03-24 ago datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-23 ago more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-22 ago ML_Lex.read_antiq;
2009-03-22 ago export eval_antiquotes: refined version that operates on ML tokens;
2009-03-20 ago report markup for ML tokens;
2009-03-19 ago eval_antiquotes: joint scanning of ML tokens and antiquotations;
2009-03-19 ago parameterized datatype antiquote and read operation;
2009-03-19 ago Antiquote.Text: keep full position information;
2009-03-19 ago OuterLex.read_antiq;
2009-03-18 ago more precise type Symbol_Pos.text;