src/Pure/ROOT.ML
Wed, 26 Mar 2014 09:13:38 +0100 wenzelm tuned load order;
Tue, 25 Mar 2014 19:03:02 +0100 wenzelm proper configuration option "ML_print_depth";
Thu, 20 Mar 2014 19:24:51 +0100 wenzelm tuned error, according to "use" in General/secure.ML;
Tue, 18 Mar 2014 18:09:31 +0100 wenzelm clarified module arrangement;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Tue, 18 Mar 2014 16:44:51 +0100 wenzelm clarified module arrangement;
Tue, 18 Mar 2014 16:16:28 +0100 wenzelm clarified modules;
Tue, 18 Mar 2014 13:36:28 +0100 wenzelm clarified bootstrap process: switch to ML with context and antiquotations earlier;
Wed, 12 Mar 2014 22:57:50 +0100 wenzelm tuned signature -- clarified module name;
Tue, 11 Mar 2014 18:26:47 +0100 wenzelm tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
Sat, 22 Feb 2014 20:52:43 +0100 wenzelm support for completion within the formal context;
Sun, 16 Feb 2014 17:25:03 +0100 wenzelm prefer user-space tool within Pure.thy;
Mon, 10 Feb 2014 22:39:04 +0100 wenzelm seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
Sat, 25 Jan 2014 18:34:05 +0100 wenzelm prefer self-contained user-space tool;
Fri, 17 Jan 2014 20:31:39 +0100 wenzelm prefer user-space tool within Pure.thy;
Fri, 13 Dec 2013 20:20:15 +0100 wenzelm maintain morphism names for diagnostic purposes;
Wed, 11 Dec 2013 18:02:22 +0100 wenzelm support for polml-5.5.2;
Sat, 16 Nov 2013 17:39:11 +0100 wenzelm toplevel function "use" refers to raw ML bootstrap environment;
Wed, 18 Sep 2013 13:31:44 +0200 wenzelm updated to polyml-5.5.1;
Wed, 18 Sep 2013 13:18:51 +0200 wenzelm improved printing of exception trace in Poly/ML 5.5.1;
Wed, 18 Sep 2013 11:08:28 +0200 wenzelm moved module into plain Isabelle/ML user space;
Mon, 26 Aug 2013 21:56:08 +0200 wenzelm added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
Sun, 25 Aug 2013 20:32:26 +0200 wenzelm maintain goal forks as part of global execution;
Thu, 08 Aug 2013 23:52:35 +0200 wenzelm removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
Mon, 05 Aug 2013 17:14:02 +0200 wenzelm slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
Thu, 01 Aug 2013 22:47:52 +0200 wenzelm exception trace for Poly/ML 5.5.1, using regular Isabelle output;
Tue, 30 Jul 2013 18:19:16 +0200 wenzelm recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
Fri, 12 Jul 2013 11:07:02 +0200 wenzelm clarified module name;
Thu, 11 Jul 2013 14:42:11 +0200 wenzelm global management of command execution fragments;
Wed, 10 Jul 2013 23:25:28 +0200 wenzelm more abstract message channel;
Fri, 05 Jul 2013 23:10:18 +0200 wenzelm more uniform Counter in ML and Scala;
Fri, 05 Jul 2013 22:58:24 +0200 wenzelm tuned signature;
Fri, 05 Jul 2013 15:38:03 +0200 wenzelm explicit module Document_ID as source of globally unique identifiers across ML/Scala;
Wed, 03 Jul 2013 16:58:35 +0200 wenzelm tuned signature;
Sun, 30 Jun 2013 11:37:34 +0200 wenzelm backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
Thu, 27 Jun 2013 23:17:26 +0200 wenzelm manage option "proofs" within theory context -- with minor overhead for primitive inferences;
Tue, 28 May 2013 23:06:32 +0200 wenzelm explicit support for type annotations within printed syntax trees;
Sat, 25 May 2013 15:44:08 +0200 haftmann tuned structure
Fri, 17 May 2013 20:41:45 +0200 wenzelm proper option quick_and_dirty;
Fri, 17 May 2013 17:11:06 +0200 wenzelm event timer as separate service thread;
Wed, 15 May 2013 20:34:42 +0200 wenzelm moved files;
Wed, 15 May 2013 20:22:46 +0200 wenzelm maintain ProofGeneral preferences within ProofGeneral module;
Wed, 15 May 2013 17:39:41 +0200 wenzelm just one ProofGeneral module;
Tue, 14 May 2013 21:56:19 +0200 wenzelm simplified modules and exceptions;
Mon, 13 May 2013 21:42:27 +0200 wenzelm more direct output of remaining PGIP rudiments;
Mon, 13 May 2013 21:03:30 +0200 wenzelm removed obsolete PGIP material;
Sun, 12 May 2013 18:22:44 +0200 wenzelm support for system options as context-sensitive config options;
Sat, 11 May 2013 20:10:24 +0200 wenzelm removed redundant modules;
Wed, 03 Apr 2013 21:48:43 +0200 wenzelm additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
Wed, 27 Mar 2013 14:19:18 +0100 wenzelm tuned signature and module arrangement;
Mon, 25 Feb 2013 10:18:33 +0100 wenzelm tuned order of modules;
Wed, 16 Jan 2013 16:26:36 +0100 wenzelm more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
Thu, 10 Jan 2013 12:41:53 +0100 wenzelm recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
Mon, 07 Jan 2013 10:17:11 +0100 wenzelm slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
Wed, 02 Jan 2013 17:58:53 +0100 wenzelm moved files;
Thu, 13 Dec 2012 13:52:18 +0100 wenzelm identify dialogs via official serial and maintain as result message;
Wed, 12 Dec 2012 21:50:42 +0100 wenzelm support dialog via document content;
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Wed, 28 Nov 2012 17:18:53 +0100 wenzelm some support for ML runtime statistics;
less more (0) -300 -100 -60 tip