src/Pure/ML/ml_env.ML
Tue, 05 Apr 2016 18:20:25 +0200 wenzelm support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
Sun, 03 Apr 2016 23:28:48 +0200 wenzelm clarified SML name space: no access to structure PolyML;
Sat, 26 Mar 2016 16:14:46 +0100 wenzelm explicit print_depth for the sake of Spec_Check.determine_type;
Thu, 17 Mar 2016 10:21:43 +0100 wenzelm tuned signature;
Tue, 01 Mar 2016 22:49:33 +0100 wenzelm tuned signature;
Tue, 01 Mar 2016 22:11:36 +0100 wenzelm clarified modules;
Tue, 01 Mar 2016 21:10:29 +0100 wenzelm load secure.ML earlier;
Wed, 17 Feb 2016 23:06:24 +0100 wenzelm SML/NJ is no longer supported;
Thu, 06 Aug 2015 21:31:54 +0200 wenzelm evaluate ML expressions within debugger context;
Fri, 17 Jul 2015 17:17:39 +0200 wenzelm store breakpoints within ML environment;
Wed, 10 Dec 2014 19:24:54 +0100 wenzelm more careful handling of auxiliary environment structure -- allow nested ML evaluation;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Sat, 19 Apr 2014 17:23:05 +0200 wenzelm added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Tue, 18 Mar 2014 13:36:28 +0100 wenzelm clarified bootstrap process: switch to ML with context and antiquotations earlier;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Fri, 16 Apr 2010 12:51:37 +0200 wenzelm proper masking of dummy name_space;
Fri, 16 Apr 2010 11:39:08 +0200 wenzelm proper checking of ML functors (in Poly/ML 5.2 or later);
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sat, 06 Jun 2009 18:11:32 +0200 wenzelm tuned comments;
Thu, 04 Jun 2009 17:31:39 +0200 wenzelm eliminated costly registration of tokens;
Mon, 01 Jun 2009 23:28:04 +0200 wenzelm tuned signature;
Mon, 01 Jun 2009 16:12:42 +0200 wenzelm maintain tokens within common ML environment;
Mon, 01 Jun 2009 15:26:00 +0200 wenzelm moved local ML environment to separate module ML_Env;
less more (0) tip