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);