src/Tools/Code/code_runtime.ML
2016-05-26 haftmann 2016-05-26 clarified naming conventions and code for code evaluation sandwiches
2016-05-26 haftmann 2016-05-26 clarified names of variants
2016-04-28 wenzelm 2016-04-28 support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
2016-04-07 wenzelm 2016-04-07 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-03-26 wenzelm 2016-03-26 explicit print_depth for the sake of Spec_Check.determine_type;
2016-03-13 haftmann 2016-03-13 dropped junk
2016-03-01 wenzelm 2016-03-01 tuned signature;
2016-03-01 wenzelm 2016-03-01 clarified modules;
2016-03-01 wenzelm 2016-03-01 load secure.ML earlier; eliminated obsolete ml_parse.ML; tuned signature;
2016-02-17 wenzelm 2016-02-17 SML/NJ is no longer supported;
2015-09-01 wenzelm 2015-09-01 thread context for exceptions from forks, e.g. relevant when printing errors; tuned signature;
2015-08-17 wenzelm 2015-08-17 explicit debug flag for ML compiler;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2014-12-19 wenzelm 2014-12-19 tuned;
2014-12-19 wenzelm 2014-12-19 proper exception for internal program failure, not user-error;
2014-12-19 wenzelm 2014-12-19 tuned;
2014-12-10 wenzelm 2014-12-10 more careful handling of auxiliary environment structure -- allow nested ML evaluation;
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;