src/Pure/ML/ml_compiler.ML
2016-12-23 wenzelm 2016-12-23 suppress dummy id;
2016-12-23 wenzelm 2016-12-23 omit unused markup;
2016-09-05 wenzelm 2016-09-05 clarified modules;
2016-04-15 wenzelm 2016-04-15 support for Poly/ML entity ids;
2016-04-10 wenzelm 2016-04-10 proper support for recursive ML debugging;
2016-04-09 wenzelm 2016-04-09 tuned signature; proper signature for structure;
2016-04-07 wenzelm 2016-04-07 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; handle bootstrap signatures as well;
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-04-05 wenzelm 2016-04-05 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
2016-04-02 wenzelm 2016-04-02 tuned signature;
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-03-18 wenzelm 2016-03-18 discontinued slightly odd "secure" mode;
2016-03-18 wenzelm 2016-03-18 clarified modules; tuned signature;
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2016-03-03 wenzelm 2016-03-03 clarified modules;
2016-03-03 wenzelm 2016-03-03 discontinued polyml-5.3.0;
2016-03-01 wenzelm 2016-03-01 tuned signature;
2016-03-01 wenzelm 2016-03-01 load secure.ML earlier; eliminated obsolete ml_parse.ML; tuned signature;
2016-03-01 wenzelm 2016-03-01 ML debugger support in Pure (again, see 3565c9f407ec);
2016-02-23 wenzelm 2016-02-23 support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
2016-02-17 wenzelm 2016-02-17 merged
2016-02-17 wenzelm 2016-02-17 clarified file names;
2015-08-17 wenzelm 2015-08-17 explicit debug flag for ML compiler;
2015-08-06 wenzelm 2015-08-06 evaluate ML expressions within debugger context; redirected writeln/warning for ML compiler;
2014-04-19 wenzelm 2014-04-19 added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-03-27 wenzelm 2014-03-27 redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-25 wenzelm 2014-03-25 proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2013-11-11 wenzelm 2013-11-11 tuned signature;
2013-09-18 wenzelm 2013-09-18 improved printing of exception trace in Poly/ML 5.5.1;
2013-04-08 wenzelm 2013-04-08 prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
2013-02-26 wenzelm 2013-02-26 tuned signature;
2013-01-16 wenzelm 2013-01-16 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2010-08-30 wenzelm 2010-08-30 more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
2009-06-06 wenzelm 2009-06-06 added exn_message (formerly in toplevel.ML); eval/code: proper Isar runtime support; tuned signature;
2009-06-04 wenzelm 2009-06-04 added exception_position (dummy);
2009-06-01 wenzelm 2009-06-01 added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);