src/Pure/ML/ml_context.ML
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.
2008-06-28 wenzelm 2008-06-28 tuned;
2008-06-25 wenzelm 2008-06-25 re-use official outer keywords;
2008-06-24 wenzelm 2008-06-24 add_antiq: more general notion of ML antiquotation; eval_antiquotes: support blocks and background context; moved concrete antiquotations to ml_antiquote.ML;
2008-05-14 wenzelm 2008-05-14 renamed Position.path to Path.position;
2008-04-15 wenzelm 2008-04-15 removed eval_antiquotes_fn; eval: CRITICAL for now;
2008-03-29 wenzelm 2008-03-29 removed obsolete store_thm(s), cf. functional versions in pure_thy.ML; tuned;
2008-03-28 wenzelm 2008-03-28 eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context; moved old the_context to old_goals.ML;
2008-03-26 wenzelm 2008-03-26 added store_thms etc. (formerly in Thy/thm_database.ML); added bind_thm(s) (formerly in old_goals.ML); adapted to Context.thread_data interface; removed obsolete get/set_context; renamed ML_Context.>> to Context.>> (again);
2008-03-26 wenzelm 2008-03-26 removed obsolete pass, save;
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-03-24 wenzelm 2008-03-24 simplified thm_antiq;
2008-03-20 wenzelm 2008-03-20 thm_antiq: produce error at runtime, not compile time; tuned;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument; renamed former get_thm to get_fact_single, and get_thms to get_fact;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-14 haftmann 2008-03-14 added mk_const functions
2008-03-01 wenzelm 2008-03-01 added @{const} antiquotation;
2008-01-01 wenzelm 2008-01-01 eval_wrapper: CRITICAL; tuned;
2007-12-18 wenzelm 2007-12-18 named some critical sections; eval_antiquotes: tightened critical section;
2007-11-08 wenzelm 2007-11-08 renamed ProofContext.read_const' to ProofContext.read_const_proper;
2007-11-07 wenzelm 2007-11-07 ProofContext.read_const';
2007-10-26 wenzelm 2007-10-26 replaced Secure.evaluate by ML_Context.evaluate;
2007-10-22 wenzelm 2007-10-22 added @{sort}, @{type_syntax} antiquotations;
2007-09-24 wenzelm 2007-09-24 added @{type_name};
2007-09-23 wenzelm 2007-09-23 tuned @{cpat};
2007-09-15 wenzelm 2007-09-15 tuned comments;
2007-09-14 wenzelm 2007-09-14 moved ML_XXX.ML files to Pure/ML;