src/Pure/ML/ml_context.ML
2014-03-18 wenzelm 2014-03-18 tuned signature -- rearranged modules;
2014-03-12 wenzelm 2014-03-12 ML_Context.check_antiquotation still required;
2014-03-12 wenzelm 2014-03-12 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
2014-03-10 wenzelm 2014-03-10 clarified Args.check_src: retain name space information for error output; tuned signature;
2014-03-10 wenzelm 2014-03-10 clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
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-25 wenzelm 2014-02-25 proper context for global data;
2014-02-17 wenzelm 2014-02-17 more markup;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context; subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);
2013-08-23 wenzelm 2013-08-23 discontinued unused antiquotation blocks;
2013-08-16 wenzelm 2013-08-16 more markup via Name_Space.check; tuned signature;
2013-07-15 wenzelm 2013-07-15 retain compile-time context visibility, which is particularly important for "apply tactic";
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-12 wenzelm 2012-08-12 more static antiquotations;
2012-08-11 wenzelm 2012-08-11 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-07-08 wenzelm 2011-07-08 clarified Thy_Load.digest_file -- read ML files only once;
2011-06-27 wenzelm 2011-06-27 proper checking of @{ML_antiquotation};
2011-06-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-09 wenzelm 2011-01-09 ML_trace: observe context visibility flag (import for Latex mode, for example);
2010-12-21 wenzelm 2010-12-21 configuration option "ML_trace";
2010-10-01 haftmann 2010-10-01 moved ML_Context.value to Code_Runtime
2010-09-30 haftmann 2010-09-30 value uses bare compiler invocation: generated code does not contain antiquotations
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-09-15 haftmann 2010-09-15 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
2010-09-06 wenzelm 2010-09-06 ML_Context.thm and ML_Context.thms no longer pervasive;
2010-09-06 wenzelm 2010-09-06 ML_Context.ml_store_thm(s): operate on thread context instead of Unsynchronized.ref;
2010-08-31 haftmann 2010-08-31 evaluate takes ml context and ml expression parameter
2010-08-25 wenzelm 2010-08-25 ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
2010-08-08 wenzelm 2010-08-08 prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
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-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-02-07 wenzelm 2010-02-07 simplified interface for ML antiquotations, struct_name is always "Isabelle";
2009-10-27 wenzelm 2009-10-27 critical comments;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-06-01 wenzelm 2009-06-01 structure ML_Compiler;
2009-06-01 wenzelm 2009-06-01 moved local ML environment to separate module ML_Env;
2009-03-24 wenzelm 2009-03-24 datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-23 wenzelm 2009-03-23 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-22 wenzelm 2009-03-22 ML_Lex.read_antiq;
2009-03-22 wenzelm 2009-03-22 export eval_antiquotes: refined version that operates on ML tokens;
2009-03-20 wenzelm 2009-03-20 report markup for ML tokens;
2009-03-19 wenzelm 2009-03-19 eval_antiquotes: joint scanning of ML tokens and antiquotations;
2009-03-19 wenzelm 2009-03-19 parameterized datatype antiquote and read operation;
2009-03-19 wenzelm 2009-03-19 Antiquote.Text: keep full position information;
2009-03-19 wenzelm 2009-03-19 OuterLex.read_antiq;
2009-03-18 wenzelm 2009-03-18 more precise type Symbol_Pos.text; geralized ML_Context.inherit_env;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-09-29 wenzelm 2008-09-29 back to plain Position.report for regular references;