src/Tools/Code/code_runtime.ML
2017-02-06 haftmann 2017-02-06 more explicit errors in pathological cases
2017-02-06 haftmann 2017-02-06 more computation antiquotations
2017-02-06 haftmann 2017-02-06 computations and partiality
2017-02-06 haftmann 2017-02-06 tuned
2017-01-27 haftmann 2017-01-27 ML antiquotation for generated computations
2017-01-26 haftmann 2017-01-26 tuned
2017-01-26 haftmann 2017-01-26 tuned structure and terminology
2017-01-26 haftmann 2017-01-26 tuned scope of lazy computation
2017-01-26 haftmann 2017-01-26 tuned data structure
2017-01-26 haftmann 2017-01-26 dropped dead code
2017-01-24 haftmann 2017-01-24 dropped dead code
2017-01-24 haftmann 2017-01-24 ensure no duplicates after preprocessing
2017-01-24 haftmann 2017-01-24 reject polymorphic result types; formally generalized to multiple result types
2017-01-24 haftmann 2017-01-24 explicit a-priori detection of unsuitable terms for computations
2017-01-22 haftmann 2017-01-22 experimental computations: use arbitrary generated code for RHSs, not just constants
2017-01-21 haftmann 2017-01-21 corrected static scope: multi-argument composition does not apply partially
2016-05-30 wenzelm 2016-05-30 merged
2016-05-28 wenzelm 2016-05-28 clarified 'axiomatization';
2016-05-29 haftmann 2016-05-29 do not export abstract constructors in code_reflect
2016-05-26 haftmann 2016-05-26 optional timing for code generator conversions
2016-05-26 haftmann 2016-05-26 clarified internal interfaces
2016-05-26 haftmann 2016-05-26 corrected closure scope of static_conv_thingol; clarified implementation and names
2016-05-26 haftmann 2016-05-26 clarified proof context vs. background theory
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