Thu, 24 Jul 2014 15:54:56 +0200 |
wenzelm |
further distinction of Isabelle distribution: alert for identified release candidates;
|
file |
diff |
annotate
|
Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
Sun, 06 Apr 2014 15:19:22 +0200 |
wenzelm |
clarified ML bootstrap;
|
file |
diff |
annotate
|
Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
Wed, 26 Mar 2014 09:19:04 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
Wed, 26 Mar 2014 09:13:38 +0100 |
wenzelm |
tuned load order;
|
file |
diff |
annotate
|
Tue, 25 Mar 2014 19:03:02 +0100 |
wenzelm |
proper configuration option "ML_print_depth";
|
file |
diff |
annotate
|
Thu, 20 Mar 2014 19:24:51 +0100 |
wenzelm |
tuned error, according to "use" in General/secure.ML;
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 18:09:31 +0100 |
wenzelm |
clarified module arrangement;
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 17:39:03 +0100 |
wenzelm |
clarifed module name;
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 16:44:51 +0100 |
wenzelm |
clarified module arrangement;
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 16:16:28 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 13:36:28 +0100 |
wenzelm |
clarified bootstrap process: switch to ML with context and antiquotations earlier;
|
file |
diff |
annotate
|
Wed, 12 Mar 2014 22:57:50 +0100 |
wenzelm |
tuned signature -- clarified module name;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Sat, 22 Feb 2014 20:52:43 +0100 |
wenzelm |
support for completion within the formal context;
|
file |
diff |
annotate
|
Sun, 16 Feb 2014 17:25:03 +0100 |
wenzelm |
prefer user-space tool within Pure.thy;
|
file |
diff |
annotate
|
Mon, 10 Feb 2014 22:39:04 +0100 |
wenzelm |
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
|
file |
diff |
annotate
|
Sat, 25 Jan 2014 18:34:05 +0100 |
wenzelm |
prefer self-contained user-space tool;
|
file |
diff |
annotate
|
Fri, 17 Jan 2014 20:31:39 +0100 |
wenzelm |
prefer user-space tool within Pure.thy;
|
file |
diff |
annotate
|
Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
file |
diff |
annotate
|
Wed, 11 Dec 2013 18:02:22 +0100 |
wenzelm |
support for polml-5.5.2;
|
file |
diff |
annotate
|
Sat, 16 Nov 2013 17:39:11 +0100 |
wenzelm |
toplevel function "use" refers to raw ML bootstrap environment;
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 13:31:44 +0200 |
wenzelm |
updated to polyml-5.5.1;
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 13:18:51 +0200 |
wenzelm |
improved printing of exception trace in Poly/ML 5.5.1;
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 11:08:28 +0200 |
wenzelm |
moved module into plain Isabelle/ML user space;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Sun, 25 Aug 2013 20:32:26 +0200 |
wenzelm |
maintain goal forks as part of global execution;
|
file |
diff |
annotate
|
Thu, 08 Aug 2013 23:52:35 +0200 |
wenzelm |
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Thu, 01 Aug 2013 22:47:52 +0200 |
wenzelm |
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
Fri, 12 Jul 2013 11:07:02 +0200 |
wenzelm |
clarified module name;
|
file |
diff |
annotate
|
Thu, 11 Jul 2013 14:42:11 +0200 |
wenzelm |
global management of command execution fragments;
|
file |
diff |
annotate
|
Wed, 10 Jul 2013 23:25:28 +0200 |
wenzelm |
more abstract message channel;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 23:10:18 +0200 |
wenzelm |
more uniform Counter in ML and Scala;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 22:58:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 16:58:35 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 30 Jun 2013 11:37:34 +0200 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
Thu, 27 Jun 2013 23:17:26 +0200 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file |
diff |
annotate
|
Tue, 28 May 2013 23:06:32 +0200 |
wenzelm |
explicit support for type annotations within printed syntax trees;
|
file |
diff |
annotate
|
Sat, 25 May 2013 15:44:08 +0200 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
Fri, 17 May 2013 17:11:06 +0200 |
wenzelm |
event timer as separate service thread;
|
file |
diff |
annotate
|
Wed, 15 May 2013 20:34:42 +0200 |
wenzelm |
moved files;
|
file |
diff |
annotate
|
Wed, 15 May 2013 20:22:46 +0200 |
wenzelm |
maintain ProofGeneral preferences within ProofGeneral module;
|
file |
diff |
annotate
|
Wed, 15 May 2013 17:39:41 +0200 |
wenzelm |
just one ProofGeneral module;
|
file |
diff |
annotate
|
Tue, 14 May 2013 21:56:19 +0200 |
wenzelm |
simplified modules and exceptions;
|
file |
diff |
annotate
|
Mon, 13 May 2013 21:42:27 +0200 |
wenzelm |
more direct output of remaining PGIP rudiments;
|
file |
diff |
annotate
|
Mon, 13 May 2013 21:03:30 +0200 |
wenzelm |
removed obsolete PGIP material;
|
file |
diff |
annotate
|
Sun, 12 May 2013 18:22:44 +0200 |
wenzelm |
support for system options as context-sensitive config options;
|
file |
diff |
annotate
|
Sat, 11 May 2013 20:10:24 +0200 |
wenzelm |
removed redundant modules;
|
file |
diff |
annotate
|
Wed, 03 Apr 2013 21:48:43 +0200 |
wenzelm |
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
|
file |
diff |
annotate
|
Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
Mon, 25 Feb 2013 10:18:33 +0100 |
wenzelm |
tuned order of modules;
|
file |
diff |
annotate
|
Wed, 16 Jan 2013 16:26:36 +0100 |
wenzelm |
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
|
file |
diff |
annotate
|
Thu, 10 Jan 2013 12:41:53 +0100 |
wenzelm |
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
|
file |
diff |
annotate
|
Mon, 07 Jan 2013 10:17:11 +0100 |
wenzelm |
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
|
file |
diff |
annotate
|
Wed, 02 Jan 2013 17:58:53 +0100 |
wenzelm |
moved files;
|
file |
diff |
annotate
|
Thu, 13 Dec 2012 13:52:18 +0100 |
wenzelm |
identify dialogs via official serial and maintain as result message;
|
file |
diff |
annotate
|
Wed, 12 Dec 2012 21:50:42 +0100 |
wenzelm |
support dialog via document content;
|
file |
diff |
annotate
|
Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
Wed, 28 Nov 2012 17:18:53 +0100 |
wenzelm |
some support for ML runtime statistics;
|
file |
diff |
annotate
|
Mon, 26 Nov 2012 16:28:22 +0100 |
wenzelm |
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
Thu, 22 Nov 2012 13:21:02 +0100 |
wenzelm |
more abstract Sendback operations, with explicit id/exec_id properties;
|
file |
diff |
annotate
|
Tue, 16 Oct 2012 15:02:49 +0200 |
wenzelm |
more friendly handling of Pure.thy bootstrap errors;
|
file |
diff |
annotate
|
Tue, 25 Sep 2012 15:40:41 +0200 |
wenzelm |
separate module Graph_Display;
|
file |
diff |
annotate
|
Tue, 25 Sep 2012 14:32:41 +0200 |
wenzelm |
added graph encode/decode operations;
|
file |
diff |
annotate
|
Fri, 31 Aug 2012 15:25:26 +0200 |
wenzelm |
more informative error message from failed goal forks (violating old-style TTY protocol!);
|
file |
diff |
annotate
|
Tue, 28 Aug 2012 22:16:06 +0200 |
wenzelm |
discontinued centralistic changelog;
|
file |
diff |
annotate
|
Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
Wed, 22 Aug 2012 12:07:11 +0200 |
wenzelm |
clarified bootstrapping of Pure;
|
file |
diff |
annotate
|
Tue, 21 Aug 2012 21:48:32 +0200 |
wenzelm |
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
|
file |
diff |
annotate
|
Mon, 20 Aug 2012 17:05:53 +0200 |
wenzelm |
some support for inlining file content into outer syntax token language;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Wed, 08 Aug 2012 12:38:41 +0200 |
wenzelm |
simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;
|
file |
diff |
annotate
|
Sun, 05 Aug 2012 13:42:21 +0200 |
wenzelm |
prefer general Command_Line.tool wrapper (cf. Scala version);
|
file |
diff |
annotate
|
Thu, 02 Aug 2012 12:36:54 +0200 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|
Wed, 01 Aug 2012 23:33:26 +0200 |
wenzelm |
more standard bootstrapping of Pure outer syntax;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Sat, 21 Jul 2012 16:41:55 +0200 |
wenzelm |
some actual build function on ML side;
|
file |
diff |
annotate
|
Thu, 24 May 2012 15:33:45 +0200 |
wenzelm |
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
|
file |
diff |
annotate
|
Thu, 24 May 2012 15:01:17 +0200 |
wenzelm |
discontinued support for Poly/ML 5.2.1;
|
file |
diff |
annotate
|
Fri, 27 Apr 2012 21:44:44 +0200 |
wenzelm |
made Context_Position independent from Config;
|
file |
diff |
annotate
|
Wed, 04 Apr 2012 14:19:47 +0200 |
wenzelm |
separate module for prover command execution;
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 20:00:13 +0100 |
wenzelm |
basic support for bundled declarations;
|
file |
diff |
annotate
|
Thu, 01 Dec 2011 14:29:14 +0100 |
wenzelm |
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
|
file |
diff |
annotate
|
Tue, 29 Nov 2011 20:18:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 29 Nov 2011 19:49:36 +0100 |
wenzelm |
rearranged files;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
Fri, 23 Sep 2011 17:23:54 +0200 |
wenzelm |
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
|
file |
diff |
annotate
|
Thu, 22 Sep 2011 20:33:08 +0200 |
wenzelm |
abstract System_Channel in ML (cf. Scala version);
|
file |
diff |
annotate
|
Wed, 21 Sep 2011 17:50:25 +0200 |
wenzelm |
slightly more general Socket_IO as part of Pure;
|
file |
diff |
annotate
|
Sun, 04 Sep 2011 15:21:50 +0200 |
wenzelm |
moved XML/YXML to src/Pure/PIDE;
|
file |
diff |
annotate
|
Sat, 27 Aug 2011 17:26:14 +0200 |
wenzelm |
explicit markup for legacy warnings;
|
file |
diff |
annotate
|
Wed, 17 Aug 2011 22:14:22 +0200 |
wenzelm |
more systematic handling of parallel exceptions;
|
file |
diff |
annotate
|
Sat, 13 Aug 2011 20:20:36 +0200 |
wenzelm |
provide node header via Scala layer;
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 20:12:36 +0200 |
wenzelm |
moved old code generator to src/Tools/;
|
file |
diff |
annotate
|
Mon, 08 Aug 2011 21:11:10 +0200 |
wenzelm |
modernized file proof_checker.ML;
|
file |
diff |
annotate
|
Sat, 23 Jul 2011 17:22:28 +0200 |
wenzelm |
explicit structure ML_System;
|
file |
diff |
annotate
|
Sat, 16 Jul 2011 20:52:41 +0200 |
wenzelm |
moved bash operations to Isabelle_System (cf. Scala version);
|
file |
diff |
annotate
|
Sat, 16 Jul 2011 18:20:02 +0200 |
wenzelm |
more general bash_process, which allows to terminate background processes as well;
|
file |
diff |
annotate
|
Wed, 13 Jul 2011 21:44:15 +0200 |
wenzelm |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
file |
diff |
annotate
|
Wed, 13 Jul 2011 20:36:18 +0200 |
wenzelm |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
|
file |
diff |
annotate
|
Wed, 13 Jul 2011 10:57:09 +0200 |
wenzelm |
XML.pretty with depth limit;
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 15:17:37 +0200 |
wenzelm |
discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 10:44:30 +0200 |
wenzelm |
tuned XML modules;
|
file |
diff |
annotate
|
Mon, 11 Jul 2011 16:48:02 +0200 |
wenzelm |
JVM method invocation service via Scala layer;
|
file |
diff |
annotate
|
Mon, 11 Jul 2011 11:13:33 +0200 |
wenzelm |
some support for raw messages, which bypass standard Symbol/YXML decoding;
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 16:34:17 +0200 |
wenzelm |
XML data representation of lambda terms;
|
file |
diff |
annotate
|
Fri, 08 Jul 2011 21:44:47 +0200 |
wenzelm |
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
|
file |
diff |
annotate
|
Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 16:31:50 +0200 |
wenzelm |
print Path.T with some markup;
|
file |
diff |
annotate
|
Sat, 25 Jun 2011 17:17:49 +0200 |
wenzelm |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
file |
diff |
annotate
|
Sat, 30 Apr 2011 19:50:39 +0200 |
wenzelm |
railroad diagrams in LaTeX as document antiquotation;
|
file |
diff |
annotate
|