src/Pure/ML/ml_compiler.ML
Tue, 01 Mar 2016 19:42:59 +0100 wenzelm ML debugger support in Pure (again, see 3565c9f407ec);
Tue, 23 Feb 2016 16:20:12 +0100 wenzelm support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
Wed, 17 Feb 2016 23:29:35 +0100 wenzelm merged
Wed, 17 Feb 2016 23:15:47 +0100 wenzelm clarified file names;
Mon, 17 Aug 2015 16:27:12 +0200 wenzelm explicit debug flag for ML compiler;
Thu, 06 Aug 2015 21:31:54 +0200 wenzelm evaluate ML expressions within debugger context;
Sat, 19 Apr 2014 17:23:05 +0200 wenzelm added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
Thu, 27 Mar 2014 17:56:13 +0100 wenzelm 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);
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
Tue, 25 Mar 2014 19:03:02 +0100 wenzelm proper configuration option "ML_print_depth";
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Mon, 11 Nov 2013 20:00:53 +0100 wenzelm tuned signature;
Wed, 18 Sep 2013 13:18:51 +0200 wenzelm improved printing of exception trace in Poly/ML 5.5.1;
Mon, 08 Apr 2013 17:10:49 +0200 wenzelm prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
Tue, 26 Feb 2013 19:58:27 +0100 wenzelm tuned signature;
Wed, 16 Jan 2013 20:41:29 +0100 wenzelm identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
Thu, 18 Aug 2011 17:53:32 +0200 wenzelm more careful treatment of exception serial numbers, with propagation to message channel;
Mon, 30 Aug 2010 15:09:20 +0200 wenzelm more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
Sat, 06 Jun 2009 21:11:23 +0200 wenzelm added exn_message (formerly in toplevel.ML);
Thu, 04 Jun 2009 17:31:38 +0200 wenzelm added exception_position (dummy);
Mon, 01 Jun 2009 23:28:06 +0200 wenzelm added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
less more (0) tip