| Fri, 19 Jan 2018 12:49:17 +0100 |
\----- start update Isabelle2015 --> Isabelle2017
|
file | diff | annotate |
| Sat, 05 Dec 2015 16:09:41 +0100 |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
file | diff | annotate |
| Wed, 13 Aug 2014 20:21:04 +0200 |
added option editor_syslog_limit;
|
file | diff | annotate |
| Tue, 05 Aug 2014 20:40:35 +0200 |
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
|
file | diff | annotate |
| Tue, 06 May 2014 16:05:14 +0200 |
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
|
file | diff | annotate |
| Fri, 25 Apr 2014 23:47:39 +0200 |
suppress potential dangerous option (see 1baa5d19ac44);
|
file | diff | annotate |
| Thu, 17 Apr 2014 11:31:46 +0200 |
tuned option name;
|
file | diff | annotate |
| Tue, 25 Mar 2014 16:54:38 +0100 |
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
|
file | diff | annotate |
| Mon, 24 Mar 2014 12:00:17 +0100 |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file | diff | annotate |
| Sat, 22 Feb 2014 20:52:43 +0100 |
support for completion within the formal context;
|
file | diff | annotate |
| Sun, 25 Aug 2013 16:03:12 +0200 |
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
|
file | diff | annotate |
| Wed, 31 Jul 2013 12:46:53 +0200 |
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
|
file | diff | annotate |
| Wed, 31 Jul 2013 10:54:37 +0200 |
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
|
file | diff | annotate |
| Tue, 30 Jul 2013 18:19:16 +0200 |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
file | diff | annotate |
| Mon, 29 Jul 2013 20:46:21 +0200 |
NEWS;
|
file | diff | annotate |
| Mon, 29 Jul 2013 16:01:05 +0200 |
afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;
|
file | diff | annotate |
| Mon, 29 Jul 2013 12:50:16 +0200 |
support declarative editor_execution_range, instead of old-style check/cancel buttons;
|
file | diff | annotate |
| Sat, 27 Jul 2013 22:20:25 +0200 |
discontinued historic document formats;
|
file | diff | annotate |
| Sat, 20 Jul 2013 16:27:55 +0200 |
option editor_execution_priority;
|
file | diff | annotate |
| Sat, 20 Jul 2013 16:18:17 +0200 |
obscure options;
|
file | diff | annotate |
| Fri, 19 Jul 2013 17:58:57 +0200 |
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 |
| Thu, 18 Jul 2013 22:18:20 +0200 |
proper system options for 'find_theorems';
|
file | diff | annotate |
| Sun, 30 Jun 2013 12:40:55 +0200 |
tuned;
|
file | diff | annotate |
| Sun, 30 Jun 2013 12:30:02 +0200 |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
|
file | diff | annotate |
| Sat, 18 May 2013 12:41:31 +0200 |
explicit notion of public options, which are shown in the editor options dialog;
|
file | diff | annotate |
| Thu, 16 May 2013 21:48:01 +0200 |
more system options as context-sensitive config options;
|
file | diff | annotate |
| Thu, 16 May 2013 21:09:58 +0200 |
Thy_Output.modes as proper option;
|
file | diff | annotate |
| Mon, 13 May 2013 19:52:16 +0200 |
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
|
file | diff | annotate |
| Mon, 13 May 2013 13:23:13 +0200 |
option "goals_limit", with more uniform description;
|
file | diff | annotate |
| Wed, 27 Mar 2013 21:25:33 +0100 |
discontinued obsolete parallel_proofs_reuse_timing;
|
file | diff | annotate |
| Wed, 27 Mar 2013 16:46:52 +0100 |
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
|
file | diff | annotate |
| Wed, 27 Mar 2013 16:38:25 +0100 |
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 |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
|
file | diff | annotate |
| Wed, 20 Feb 2013 19:57:17 +0100 |
option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
|
file | diff | annotate |
| Tue, 22 Jan 2013 11:28:54 +0100 |
more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
|
file | diff | annotate |
| Thu, 03 Jan 2013 14:03:44 +0100 |
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
|
file | diff | annotate |
| Thu, 03 Jan 2013 13:54:45 +0100 |
improved Monitor_Dockable, based on ML_Statistics operations;
|
file | diff | annotate |
| Thu, 13 Dec 2012 19:53:55 +0100 |
smarter handling of tracing messages: prover process pauses and enters user dialog;
|
file | diff | annotate |
| Mon, 10 Dec 2012 16:06:57 +0100 |
more generous tracing limit -- rescaled in MB;
|
file | diff | annotate |
| Wed, 28 Nov 2012 17:18:53 +0100 |
some support for ML runtime statistics;
|
file | diff | annotate |
| Sun, 18 Nov 2012 19:01:30 +0100 |
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
|
file | diff | annotate |
| Sun, 18 Nov 2012 16:04:13 +0100 |
more generous tracing_limit, with explicit system option;
|
file | diff | annotate |
| Sat, 22 Sep 2012 14:41:41 +0200 |
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
|
file | diff | annotate |
| Tue, 11 Sep 2012 22:59:25 +0200 |
more precise sections;
|
file | diff | annotate |
| Tue, 11 Sep 2012 19:43:06 +0200 |
tuned;
|
file | diff | annotate |
| Tue, 11 Sep 2012 19:19:39 +0200 |
more options;
|
file | diff | annotate |
| Tue, 11 Sep 2012 15:47:42 +0200 |
some support to organize options in sections;
|
file | diff | annotate |
| Tue, 14 Aug 2012 15:42:58 +0200 |
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
|
file | diff | annotate |
| Tue, 14 Aug 2012 13:01:09 +0200 |
clarified format of etc/options: only declarations, not re-definitions;
|
file | diff | annotate |
| Fri, 03 Aug 2012 14:52:45 +0200 |
timeout for session build job;
|
file | diff | annotate |
| Wed, 01 Aug 2012 15:46:45 +0200 |
explicit option skip_proofs;
|
file | diff | annotate |
| Sat, 28 Jul 2012 19:37:35 +0200 |
some description of main build options;
|
file | diff | annotate |
| Thu, 26 Jul 2012 19:41:05 +0200 |
more build options;
|
file | diff | annotate |
| Thu, 26 Jul 2012 17:17:53 +0200 |
more build options;
|
file | diff | annotate |
| Thu, 26 Jul 2012 14:29:54 +0200 |
refined "document_dump_mode": "all", "tex+sty", "tex";
|
file | diff | annotate |
| Thu, 26 Jul 2012 13:38:43 +0200 |
discontinued slightly odd "browser_info_remote" -- it could point to a completely different version of the Isabelle library;
|
file | diff | annotate |
| Tue, 24 Jul 2012 21:54:49 +0200 |
more build options;
|
file | diff | annotate |
| Tue, 24 Jul 2012 21:26:28 +0200 |
more build options;
|
file | diff | annotate |
| Tue, 24 Jul 2012 12:20:01 +0200 |
added "document_dump_only" (cf. negated usedir -C);
|
file | diff | annotate |
| Tue, 24 Jul 2012 11:39:22 +0200 |
further imitation of ISABELLE_USEDIR_OPTIONS via options;
|
file | diff | annotate |