Sat, 08 Apr 2017 21:28:19 +0200 |
wenzelm |
provide Resources.import_name in ML, similar to Scala version;
|
file |
diff |
annotate
|
Sat, 08 Apr 2017 20:56:41 +0200 |
wenzelm |
more session_base information in ML;
|
file |
diff |
annotate
|
Fri, 07 Apr 2017 19:35:39 +0200 |
wenzelm |
provide session base for "isabelle build" and "isabelle console" ML process;
|
file |
diff |
annotate
|
Sun, 19 Mar 2017 11:56:56 +0100 |
wenzelm |
eliminated somewhat redundant inlined name (despite a7aa17a1f721);
|
file |
diff |
annotate
|
Sat, 18 Mar 2017 20:51:42 +0100 |
wenzelm |
more realistic PIDE build session;
|
file |
diff |
annotate
|
Sat, 18 Mar 2017 16:15:37 +0100 |
wenzelm |
more explicit build_session args;
|
file |
diff |
annotate
|
Sat, 18 Mar 2017 14:30:03 +0100 |
wenzelm |
avoid compiler warning;
|
file |
diff |
annotate
|
Mon, 27 Feb 2017 16:29:52 +0100 |
wenzelm |
absent timing information means zero, according to 0070053570c4, f235646b1b73;
|
file |
diff |
annotate
|
Sun, 18 Dec 2016 15:53:27 +0100 |
wenzelm |
dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);
|
file |
diff |
annotate
|
Wed, 19 Oct 2016 14:42:28 +0200 |
wenzelm |
added system option "profiling";
|
file |
diff |
annotate
|
Thu, 08 Sep 2016 18:18:57 +0200 |
wenzelm |
option "checkpoint" helps to fine-tune global heap space management;
|
file |
diff |
annotate
|
Sat, 09 Apr 2016 16:16:05 +0200 |
wenzelm |
shared output primitives of physical/virtual Pure;
|
file |
diff |
annotate
|
Sat, 09 Apr 2016 14:17:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 06 Apr 2016 11:44:34 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
Fri, 01 Apr 2016 17:00:18 +0200 |
wenzelm |
less bulky timing information, e.g. HOL 56913 ~> 672;
|
file |
diff |
annotate
|
Sat, 26 Mar 2016 14:27:58 +0100 |
wenzelm |
obsolete -- done in Isabelle_Process.init_options;
|
file |
diff |
annotate
|
Sat, 26 Mar 2016 14:14:23 +0100 |
wenzelm |
clarified use of options;
|
file |
diff |
annotate
|
Sat, 26 Mar 2016 13:41:14 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 18 Mar 2016 17:11:30 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Tue, 15 Mar 2016 16:23:27 +0100 |
wenzelm |
ML save_state under control of Isabelle/Scala;
|
file |
diff |
annotate
|
Sat, 12 Mar 2016 20:17:37 +0100 |
wenzelm |
clarified session build options: already provided by ML_Process;
|
file |
diff |
annotate
|
Mon, 29 Feb 2016 16:25:51 +0100 |
wenzelm |
redundant -- already part of Session.finish;
|
file |
diff |
annotate
|
Mon, 29 Feb 2016 16:12:47 +0100 |
wenzelm |
save heap more directly;
|
file |
diff |
annotate
|
Sat, 10 Oct 2015 16:21:34 +0200 |
wenzelm |
more explicit HTML.symbols;
|
file |
diff |
annotate
|
Fri, 09 Oct 2015 19:25:13 +0200 |
wenzelm |
output HTML text according to Isabelle/Scala Symbol.Interpretation;
|
file |
diff |
annotate
|
Sun, 25 Jan 2015 22:11:06 +0100 |
wenzelm |
discontinued obsolete option "document_graph";
|
file |
diff |
annotate
|
Sun, 25 Jan 2015 21:46:21 +0100 |
wenzelm |
provide session_graph.pdf via Isabelle/Scala;
|
file |
diff |
annotate
|
Thu, 15 Jan 2015 12:54:08 +0100 |
wenzelm |
more informative build_theories_result: cumulative Runtime.exn_message;
|
file |
diff |
annotate
|
Thu, 15 Jan 2015 11:39:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 14 Jan 2015 16:27:19 +0100 |
wenzelm |
clarified build_theories: proper protocol handler;
|
file |
diff |
annotate
|
Wed, 14 Jan 2015 14:28:52 +0100 |
wenzelm |
clarified build_theories;
|
file |
diff |
annotate
|
Tue, 13 Jan 2015 21:46:09 +0100 |
wenzelm |
some support for PIDE batch session;
|
file |
diff |
annotate
|
Mon, 22 Dec 2014 16:44:24 +0100 |
wenzelm |
system option "pretty_margin" is superseded by "thy_output_margin";
|
file |
diff |
annotate
|
Thu, 18 Dec 2014 21:10:39 +0100 |
wenzelm |
suppress irrelevant timing messages (the majority);
|
file |
diff |
annotate
|
Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
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
|
Fri, 31 Oct 2014 18:56:59 +0100 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
file |
diff |
annotate
|
Tue, 22 Apr 2014 12:30:54 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 17 Apr 2014 12:03:15 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
Thu, 17 Apr 2014 11:42:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 17 Apr 2014 11:29:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 11:52:28 +0200 |
wenzelm |
explicit 'document_files' in session ROOT specifications;
|
file |
diff |
annotate
|
Thu, 10 Apr 2014 18:13:44 +0200 |
wenzelm |
removed obsolete doc_dump option (see also 892061142ba6);
|
file |
diff |
annotate
|
Thu, 13 Feb 2014 12:09:51 +0100 |
wenzelm |
explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
|
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
|
Wed, 11 Dec 2013 18:02:22 +0100 |
wenzelm |
support for polml-5.5.2;
|
file |
diff |
annotate
|
Sat, 16 Nov 2013 22:17:45 +0100 |
wenzelm |
prefer explicit "document" flag -- eliminated stateful Present.no_document;
|
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
|
Fri, 02 Aug 2013 20:47:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 19 Jul 2013 17:58:57 +0200 |
wenzelm |
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
|
file |
diff |
annotate
|
Sun, 30 Jun 2013 12:30:02 +0200 |
wenzelm |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
|
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, 21 May 2013 17:55:28 +0200 |
wenzelm |
proper options;
|
file |
diff |
annotate
|
Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
Fri, 17 May 2013 18:19:42 +0200 |
wenzelm |
discontinued obsolete isabelle usedir, mkdir, make;
|
file |
diff |
annotate
|
Thu, 16 May 2013 20:50:01 +0200 |
wenzelm |
some system options as context-sensitive config options;
|
file |
diff |
annotate
|
Sun, 12 May 2013 20:25:45 +0200 |
wenzelm |
some system options as context-sensitive config options;
|
file |
diff |
annotate
|
Sun, 12 May 2013 15:05:15 +0200 |
wenzelm |
full default options for Isabelle_Process and Build;
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 21:22:15 +0200 |
wenzelm |
add command timings (like document command status);
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 20:16:52 +0200 |
wenzelm |
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 15:59:02 +0200 |
wenzelm |
clarified protocol_message undefinedness;
|
file |
diff |
annotate
|
Wed, 27 Mar 2013 16:38:25 +0100 |
wenzelm |
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
|
file |
diff |
annotate
|
Wed, 13 Mar 2013 21:25:08 +0100 |
wenzelm |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
|
file |
diff |
annotate
|
Tue, 12 Mar 2013 16:47:24 +0100 |
wenzelm |
discontinued "isabelle usedir" option -r (reset session path);
|
file |
diff |
annotate
|
Mon, 11 Mar 2013 14:25:14 +0100 |
wenzelm |
discontinued "isabelle usedir" option -P (remote path);
|
file |
diff |
annotate
|
Wed, 20 Feb 2013 15:22:22 +0100 |
wenzelm |
more tight representation of command timing;
|
file |
diff |
annotate
|
Tue, 19 Feb 2013 16:49:40 +0100 |
wenzelm |
recover timing information from old log files;
|
file |
diff |
annotate
|
Tue, 19 Feb 2013 13:57:13 +0100 |
wenzelm |
support for build passing timings from Scala to ML;
|
file |
diff |
annotate
|
Tue, 19 Feb 2013 12:58:32 +0100 |
wenzelm |
support for prescient timing information within command transactions;
|
file |
diff |
annotate
|
Tue, 19 Feb 2013 10:55:11 +0100 |
wenzelm |
emit command_timing properties into build log;
|
file |
diff |
annotate
|
Thu, 24 Jan 2013 17:18:13 +0100 |
wenzelm |
more efficient inlined properties, especially relevant for voluminous tasks trace;
|
file |
diff |
annotate
|
Fri, 18 Jan 2013 23:33:17 +0100 |
wenzelm |
use inlined session name as title for charts;
|
file |
diff |
annotate
|
Fri, 18 Jan 2013 17:51:50 +0100 |
wenzelm |
more systematic task statistics;
|
file |
diff |
annotate
|
Sat, 12 Jan 2013 15:00:48 +0100 |
wenzelm |
immediate theory progress for build_dialog;
|
file |
diff |
annotate
|
Tue, 08 Jan 2013 21:16:51 +0100 |
wenzelm |
include timing properties in log;
build_history_base
|
file |
diff |
annotate
|
Thu, 03 Jan 2013 20:42:18 +0100 |
wenzelm |
maintain session index on Scala side, for more determistic results;
|
file |
diff |
annotate
|
Thu, 03 Jan 2013 14:03:44 +0100 |
wenzelm |
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
|
file |
diff |
annotate
|
Wed, 02 Jan 2013 17:58:53 +0100 |
wenzelm |
moved files;
|
file |
diff |
annotate
| base
|