src/Pure/ROOT.ML
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;
Mon, 26 Nov 2012 16:28:22 +0100 wenzelm clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 22 Nov 2012 13:21:02 +0100 wenzelm more abstract Sendback operations, with explicit id/exec_id properties;
Tue, 16 Oct 2012 15:02:49 +0200 wenzelm more friendly handling of Pure.thy bootstrap errors;
Tue, 25 Sep 2012 15:40:41 +0200 wenzelm separate module Graph_Display;
Tue, 25 Sep 2012 14:32:41 +0200 wenzelm added graph encode/decode operations;
Fri, 31 Aug 2012 15:25:26 +0200 wenzelm more informative error message from failed goal forks (violating old-style TTY protocol!);
Tue, 28 Aug 2012 22:16:06 +0200 wenzelm discontinued centralistic changelog;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Wed, 22 Aug 2012 12:07:11 +0200 wenzelm clarified bootstrapping of Pure;
Tue, 21 Aug 2012 21:48:32 +0200 wenzelm more standard Thy_Load.check_thy for Pure.thy, relying on its header;
Mon, 20 Aug 2012 17:05:53 +0200 wenzelm some support for inlining file content into outer syntax token language;
Sat, 11 Aug 2012 18:05:41 +0200 wenzelm clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
Wed, 08 Aug 2012 12:38:41 +0200 wenzelm simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;
Sun, 05 Aug 2012 13:42:21 +0200 wenzelm prefer general Command_Line.tool wrapper (cf. Scala version);
Thu, 02 Aug 2012 12:36:54 +0200 wenzelm more official command specifications, including source position;
Wed, 01 Aug 2012 23:33:26 +0200 wenzelm more standard bootstrapping of Pure outer syntax;
Mon, 23 Jul 2012 22:35:10 +0200 wenzelm added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
less more (0) -300 -100 -60 tip