2014-12-05 haftmann 2014-12-05 allow multiple inheritance of targets
2014-10-09 haftmann 2014-10-09 more foundational definition for predicate even
2014-10-09 haftmann 2014-10-09 formally completeted set of experimental static evaluation functions
2014-10-05 haftmann 2014-10-05 basic support for fully static evaluator generation without dynamic compiler invocation
2014-10-05 haftmann 2014-10-05 split dynamic from static context
2014-06-29 haftmann 2014-06-29 modernized diagnostic options
2014-05-15 haftmann 2014-05-15 syntactic means to prevent accidental mixup of static and dynamic context
2014-05-15 haftmann 2014-05-15 dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
2014-05-09 haftmann 2014-05-09 normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;
2014-04-19 wenzelm 2014-04-19 added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;
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-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-02-23 haftmann 2014-02-23 keep only identifiers public which are explicitly requested or demanded by dependencies
2014-02-23 haftmann 2014-02-23 explicit option for "open" code generation
2014-02-03 wenzelm 2014-02-03 more formal markup;
2014-01-30 haftmann 2014-01-30 reduced prominence of "permissive code generation"
2014-01-25 haftmann 2014-01-25 less clumsy namespace
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