src/Pure/ML/ml_context.ML
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;
2008-09-29 wenzelm 2008-09-29 ContextPosition.report; parse_token/report_token: explicit context;
2008-09-17 wenzelm 2008-09-17 added inherit_env;
2008-09-17 wenzelm 2008-09-17 explicit handling of ML environment within generic context; eval_wrapper: non-critical, struct_name is always Isabelle, tuned comments; eval_in/evaluate expect immutable Proof.context value; use_text/use_file now depend on explicit ML name space;
2008-08-15 wenzelm 2008-08-15 report antiquotation names;
2008-08-14 wenzelm 2008-08-14 report ML_source;
2008-08-14 wenzelm 2008-08-14 antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-14 wenzelm 2008-08-14 ML_Context.add_antiq: pass position;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-08-07 wenzelm 2008-08-07 simplified Antiquote signature;
2008-08-07 wenzelm 2008-08-07 Antiquote.read/read_arguments;
2008-08-06 wenzelm 2008-08-06 adapted Antiq;
2008-08-04 berghofe 2008-08-04 Exported eval_wrapper.