2014-03-27 ago tuned;
2014-03-27 ago 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);
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-25 ago proper configuration option "ML_print_depth";
2014-03-25 ago added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-24 ago discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-02 ago clarified names of antiquotations and markup;
2013-11-11 ago tuned message;
2013-11-11 ago tuned signature;
2013-09-18 ago improved printing of exception trace in Poly/ML 5.5.1;
2013-04-08 ago prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
2013-01-16 ago identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 ago more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-16 ago tuned comments;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-12 ago more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;
2012-08-29 ago renamed Position.str_of to;
2012-05-24 ago simplified Poly/ML setup -- 5.3.0 is now the common base-line;