2017-08-08 |
wenzelm |
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
|
file |
diff |
annotate
|
2017-06-21 |
wenzelm |
tuned granularity of parallel tasks;
|
file |
diff |
annotate
|
2017-06-21 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
2017-05-08 |
wenzelm |
simplified default;
|
file |
diff |
annotate
|
2017-04-27 |
wenzelm |
support for database connection;
|
file |
diff |
annotate
|
2017-04-10 |
wenzelm |
explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
|
file |
diff |
annotate
|
2017-04-09 |
wenzelm |
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
|
file |
diff |
annotate
|
2017-03-15 |
wenzelm |
dynamic session_options for tuning parameters and initial prover options;
|
file |
diff |
annotate
|
2017-03-07 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
2017-02-26 |
wenzelm |
clarified defaults;
|
file |
diff |
annotate
|
2016-11-24 |
wenzelm |
explicit option editor_generated_input_delay, which is more aggressive by default;
|
file |
diff |
annotate
|
2016-10-20 |
wenzelm |
prevent sporadic disconnection;
|
file |
diff |
annotate
|
2016-10-19 |
wenzelm |
added system option "profiling";
|
file |
diff |
annotate
|
2016-10-10 |
wenzelm |
clarified treatment of options;
|
file |
diff |
annotate
|
2016-10-01 |
wenzelm |
options for process policy, notably for multiprocessor machines;
|
file |
diff |
annotate
|
2016-09-08 |
wenzelm |
option "checkpoint" helps to fine-tune global heap space management;
|
file |
diff |
annotate
|
2016-04-06 |
wenzelm |
simplified bootstrap: critical structures remain accessible in ML_Root context;
|
file |
diff |
annotate
|
2016-04-05 |
wenzelm |
clarified bootstrap environment;
|
file |
diff |
annotate
|
2016-04-04 |
wenzelm |
option ML_system_unsafe;
|
file |
diff |
annotate
|
2016-04-01 |
wenzelm |
lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
|
file |
diff |
annotate
|
2016-04-01 |
wenzelm |
less bulky timing information, e.g. HOL 56913 ~> 672;
|
file |
diff |
annotate
|
2016-04-01 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
2016-03-26 |
wenzelm |
avoid hardwired values;
|
file |
diff |
annotate
|
2016-03-02 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
2016-02-25 |
wenzelm |
proper option process_output_tail, more generous default;
|
file |
diff |
annotate
|
2016-01-10 |
wenzelm |
prune old versions more often, to reduce overall heap requirements;
|
file |
diff |
annotate
|
2015-12-19 |
wenzelm |
prune old document versions more frequently, for reduced heap usage;
|
file |
diff |
annotate
|
2015-11-09 |
wenzelm |
prefer explicit State panel;
|
file |
diff |
annotate
|
2015-11-08 |
wenzelm |
added option timeout_scale;
|
file |
diff |
annotate
|
2015-11-07 |
wenzelm |
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
|
file |
diff |
annotate
|
2015-11-02 |
wenzelm |
clarified completion of Isabelle symbols within document source;
|
file |
diff |
annotate
|
2015-09-21 |
wenzelm |
option editor_output_state;
|
file |
diff |
annotate
|
2015-09-11 |
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
|
2015-08-11 |
wenzelm |
init/exit depending on active debugger panels;
|
file |
diff |
annotate
|
2015-08-10 |
wenzelm |
eliminated global option: breakpoints control this individually;
|
file |
diff |
annotate
|
2015-08-05 |
wenzelm |
more controls;
|
file |
diff |
annotate
|
2015-08-05 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
2015-07-21 |
wenzelm |
support for ML debugger;
|
file |
diff |
annotate
|
2015-07-16 |
wenzelm |
added option ML_debugger;
|
file |
diff |
annotate
|
2015-04-15 |
wenzelm |
GUI controls for ML_statistics, for more digestible protocol dump;
|
file |
diff |
annotate
|
2015-01-29 |
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
|
2015-01-25 |
wenzelm |
discontinued obsolete option "document_graph";
|
file |
diff |
annotate
|
2014-12-22 |
wenzelm |
system option "pretty_margin" is superseded by "thy_output_margin";
|
file |
diff |
annotate
|
2014-10-31 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
file |
diff |
annotate
|
2014-08-13 |
wenzelm |
added option editor_syslog_limit;
|
file |
diff |
annotate
|
2014-08-05 |
wenzelm |
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
|
file |
diff |
annotate
|
2014-05-06 |
wenzelm |
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
|
file |
diff |
annotate
|
2014-04-25 |
wenzelm |
suppress potential dangerous option (see 1baa5d19ac44);
|
file |
diff |
annotate
|
2014-04-17 |
wenzelm |
tuned option name;
|
file |
diff |
annotate
|
2014-03-25 |
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
|
2014-03-24 |
wenzelm |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
file |
diff |
annotate
|
2014-02-22 |
wenzelm |
support for completion within the formal context;
|
file |
diff |
annotate
|
2013-08-25 |
wenzelm |
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
|
file |
diff |
annotate
|
2013-07-31 |
wenzelm |
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
|
file |
diff |
annotate
|
2013-07-31 |
wenzelm |
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
|
file |
diff |
annotate
|
2013-07-30 |
wenzelm |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
file |
diff |
annotate
|
2013-07-29 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
2013-07-29 |
wenzelm |
afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;
|
file |
diff |
annotate
|
2013-07-29 |
wenzelm |
support declarative editor_execution_range, instead of old-style check/cancel buttons;
|
file |
diff |
annotate
|
2013-07-27 |
wenzelm |
discontinued historic document formats;
|
file |
diff |
annotate
|