2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
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-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-23 haftmann 2013-06-23 more appropriate cutting of input syntax
2012-07-27 haftmann 2012-07-27 evaluation: allow multiple code modules
2012-04-19 haftmann 2012-04-19 dropped dead code
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-15 wenzelm 2012-03-15 prefer formally checked @{keyword} parser;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-02-29 wenzelm 2012-02-29 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
2011-11-09 wenzelm 2011-11-09 misc tuning;
2011-10-26 wenzelm 2011-10-26 tuned;
2011-09-02 haftmann 2011-09-02 avoid "Code" as structure name
2011-07-01 wenzelm 2011-07-01 proper @{binding} antiquotations (relevant for formal references);
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-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-01-09 wenzelm 2011-01-09 reverted 08240feb69c7 -- breaks positions of reports;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-21 wenzelm 2010-12-21 more robust ML antiquotations -- allow original tokens without adjacent whitespace;
2010-12-21 haftmann 2010-12-21 evaluator separating static and dynamic operations
2010-12-21 haftmann 2010-12-21 tuned naming
2010-12-21 haftmann 2010-12-21 evaluator separating static and dynamic operations
2010-12-21 haftmann 2010-12-21 program is separate argument to serializer
2010-12-17 haftmann 2010-12-17 avoid slightly odd Conv.tap_thy
2010-12-15 haftmann 2010-12-15 simplified evaluation function names
2010-12-09 haftmann 2010-12-09 tuned names
2010-12-09 haftmann 2010-12-09 tracing of term to be evaluated
2010-11-26 haftmann 2010-11-26 keep type variable arguments of datatype constructors in bookkeeping
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star
2010-11-08 haftmann 2010-11-08 corrected slip: must keep constant map, not type map; tuned code
2010-11-08 haftmann 2010-11-08 constructors to datatypes in code_reflect can be globbed; dropped unused code
2010-11-03 haftmann 2010-11-03 polyml_as_definition does not require explicit dependencies on external ML files
2010-10-29 haftmann 2010-10-29 actually pass "verbose" argument
2010-10-28 wenzelm 2010-10-28 use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
2010-10-26 haftmann 2010-10-26 Code_Runtime.trace
2010-10-01 haftmann 2010-10-01 merged
2010-10-01 haftmann 2010-10-01 avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
2010-10-01 wenzelm 2010-10-01 made SML/NJ happy;
2010-10-01 haftmann 2010-10-01 added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!
2010-09-21 haftmann 2010-09-21 reject term variables explicitly
2010-09-20 haftmann 2010-09-20 made smlnj happy
2010-09-17 haftmann 2010-09-17 closures preserve static serializer context for static evaluation; tuned
2010-09-17 haftmann 2010-09-17 made sml/nj happy
2010-09-16 haftmann 2010-09-16 dynamic and static value computation; built-in evaluation of propositions
2010-09-15 haftmann 2010-09-15 proper interface for code_reflect
2010-09-15 haftmann 2010-09-15 Code_Runtime.value, corresponding to ML_Context.value; tuned
2010-09-15 haftmann 2010-09-15 code_eval renamed to code_runtime