| Mon, 27 Feb 2017 00:00:28 +0100 |
wenzelm |
clarified defaults;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2016 15:21:54 +0100 |
wenzelm |
explicit option editor_generated_input_delay, which is more aggressive by default;
|
file |
diff |
annotate
|
| Thu, 20 Oct 2016 23:05:13 +0200 |
wenzelm |
prevent sporadic disconnection;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2016 14:42:28 +0200 |
wenzelm |
added system option "profiling";
|
file |
diff |
annotate
|
| Mon, 10 Oct 2016 11:48:24 +0200 |
wenzelm |
clarified treatment of options;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 23:05:25 +0200 |
wenzelm |
options for process policy, notably for multiprocessor machines;
|
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
|
| Wed, 06 Apr 2016 11:57:21 +0200 |
wenzelm |
simplified bootstrap: critical structures remain accessible in ML_Root context;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 19:41:58 +0200 |
wenzelm |
clarified bootstrap environment;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 20:07:08 +0200 |
wenzelm |
option ML_system_unsafe;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:13:40 +0200 |
wenzelm |
lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:00:18 +0200 |
wenzelm |
less bulky timing information, e.g. HOL 56913 ~> 672;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 16:20:04 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2016 12:22:15 +0100 |
wenzelm |
avoid hardwired values;
|
file |
diff |
annotate
|
| Wed, 02 Mar 2016 19:43:31 +0100 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2016 16:16:29 +0100 |
wenzelm |
proper option process_output_tail, more generous default;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2016 23:25:11 +0100 |
wenzelm |
prune old versions more often, to reduce overall heap requirements;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 23:25:23 +0100 |
wenzelm |
prune old document versions more frequently, for reduced heap usage;
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 13:49:56 +0100 |
wenzelm |
prefer explicit State panel;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2015 14:41:07 +0100 |
wenzelm |
added option timeout_scale;
|
file |
diff |
annotate
|
| Sat, 07 Nov 2015 16:05:28 +0100 |
wenzelm |
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 10:20:27 +0100 |
wenzelm |
clarified completion of Isabelle symbols within document source;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 16:41:20 +0200 |
wenzelm |
option editor_output_state;
|
file |
diff |
annotate
|
| Fri, 11 Sep 2015 17:57:34 +0200 |
wenzelm |
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
|
file |
diff |
annotate
|
| Tue, 11 Aug 2015 14:13:36 +0200 |
wenzelm |
init/exit depending on active debugger panels;
|
file |
diff |
annotate
|
| Mon, 10 Aug 2015 21:11:15 +0200 |
wenzelm |
eliminated global option: breakpoints control this individually;
|
file |
diff |
annotate
|
| Wed, 05 Aug 2015 16:22:56 +0200 |
wenzelm |
more controls;
|
file |
diff |
annotate
|
| Wed, 05 Aug 2015 16:13:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2015 19:04:36 +0200 |
wenzelm |
support for ML debugger;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 11:38:18 +0200 |
wenzelm |
added option ML_debugger;
|
file |
diff |
annotate
|
| Wed, 15 Apr 2015 13:55:01 +0200 |
wenzelm |
GUI controls for ML_statistics, for more digestible protocol dump;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 15:21:16 +0100 |
wenzelm |
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
|
file |
diff |
annotate
|
| Sun, 25 Jan 2015 22:11:06 +0100 |
wenzelm |
discontinued obsolete option "document_graph";
|
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
|
| Fri, 31 Oct 2014 18:56:59 +0100 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 20:21:04 +0200 |
wenzelm |
added option editor_syslog_limit;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 20:40:35 +0200 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
suppress potential dangerous option (see 1baa5d19ac44);
|
file |
diff |
annotate
|
| Thu, 17 Apr 2014 11:31:46 +0200 |
wenzelm |
tuned option name;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:54:38 +0100 |
wenzelm |
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 |
wenzelm |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file |
diff |
annotate
|
| Sat, 22 Feb 2014 20:52:43 +0100 |
wenzelm |
support for completion within the formal context;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 16:03:12 +0200 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
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 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 16:01:05 +0200 |
wenzelm |
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 |
wenzelm |
support declarative editor_execution_range, instead of old-style check/cancel buttons;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 22:20:25 +0200 |
wenzelm |
discontinued historic document formats;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2013 16:27:55 +0200 |
wenzelm |
option editor_execution_priority;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2013 16:18:17 +0200 |
wenzelm |
obscure options;
|
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
|
| Thu, 18 Jul 2013 22:18:20 +0200 |
wenzelm |
proper system options for 'find_theorems';
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 12:40:55 +0200 |
wenzelm |
tuned;
|
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
|
| Sat, 18 May 2013 12:41:31 +0200 |
wenzelm |
explicit notion of public options, which are shown in the editor options dialog;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 21:48:01 +0200 |
wenzelm |
more system options as context-sensitive config options;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 21:09:58 +0200 |
wenzelm |
Thy_Output.modes as proper option;
|
file |
diff |
annotate
|