| Sat, 02 Apr 2016 23:14:08 +0200 |
wenzelm |
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 20:33:34 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 20:23:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2016 16:14:46 +0100 |
wenzelm |
explicit print_depth for the sake of Spec_Check.determine_type;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2016 12:17:02 +0100 |
wenzelm |
eliminated duplicate;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 17:58:19 +0100 |
wenzelm |
discontinued slightly odd "secure" mode;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 17:11:30 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:38:40 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 16:56:44 +0100 |
wenzelm |
@{make_string} is available during Pure bootstrap;
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 13:44:18 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 10:54:28 +0100 |
wenzelm |
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 10:22:50 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Thu, 17 Mar 2016 10:21:43 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 22:06:05 +0100 |
wenzelm |
eliminated without magic name;
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 09:56:29 +0100 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 09:50:53 +0100 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2016 19:30:09 +0100 |
wenzelm |
isabelle.Build uses ML_Process directly;
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 21:53:21 +0100 |
wenzelm |
discontinued cd, pwd;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 13:51:21 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 21:59:21 +0100 |
wenzelm |
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 11:12:02 +0100 |
wenzelm |
discontinued polyml-5.3.0;
|
file |
diff |
annotate
|
| Wed, 02 Mar 2016 19:43:31 +0100 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 22:11:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 21:10:29 +0100 |
wenzelm |
load secure.ML earlier;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 19:42:59 +0100 |
wenzelm |
ML debugger support in Pure (again, see 3565c9f407ec);
|
file |
diff |
annotate
|
| Sun, 28 Feb 2016 21:20:51 +0100 |
wenzelm |
support only polyml-5.3.0 and polyml-5.6;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2016 23:10:28 +0100 |
wenzelm |
unconditional Multithreading;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:28:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:15:47 +0100 |
wenzelm |
clarified file names;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:06:24 +0100 |
wenzelm |
SML/NJ is no longer supported;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2015 23:10:08 +0100 |
wenzelm |
discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6;
|
file |
diff |
annotate
|
| Fri, 20 Nov 2015 21:52:05 +0100 |
wenzelm |
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2015 08:45:51 +0100 |
haftmann |
separate ML module for interpretation
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 21:31:14 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2015 13:54:34 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2015 17:29:37 +0200 |
wenzelm |
load markdown.ML into Pure;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 23:33:29 +0200 |
wenzelm |
more explicit Defs.context: use proper name spaces as far as possible;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 23:45:12 +0200 |
wenzelm |
basic setup for native Windows (RAW session without image);
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 21:32:41 +0200 |
wenzelm |
no ML_debugger support in Pure -- too complicated;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 21:22:55 +0200 |
wenzelm |
more careful propagation of ML_debugger option to Pure;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 19:34:15 +0200 |
wenzelm |
support for ML files with/without debugger information;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 16:27:12 +0200 |
wenzelm |
explicit debug flag for ML compiler;
|
file |
diff |
annotate
|
| Sat, 15 Aug 2015 19:42:35 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 01:39:31 +0200 |
wenzelm |
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2015 12:39:08 +0200 |
wenzelm |
clarified module;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:08:06 +0200 |
wenzelm |
added command 'experiment';
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 11:30:54 +0100 |
wenzelm |
tuned protocol -- resolve command positions in ML;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 16:16:01 +0100 |
wenzelm |
tuned bootstrap;
|
file |
diff |
annotate
|
| Wed, 14 Jan 2015 11:52:08 +0100 |
wenzelm |
added Path.decode in ML, in correspondence to Path.encode in Scala;
|
file |
diff |
annotate
|
| Tue, 30 Dec 2014 23:45:03 +0100 |
wenzelm |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 15:38:59 +0100 |
wenzelm |
more toplevel pretty printing;
|
file |
diff |
annotate
|
| Mon, 22 Dec 2014 14:33:53 +0100 |
wenzelm |
separate module Random;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 22:34:28 +0100 |
wenzelm |
node-specific keywords, with session base syntax as default;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 11:43:51 +0100 |
wenzelm |
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
|
file |
diff |
annotate
|
| Fri, 21 Nov 2014 18:14:39 +0100 |
wenzelm |
removed some add-ons from modules that are relevant for the inference kernel;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|