etc/options
2016-04-06 wenzelm 2016-04-06 simplified bootstrap: critical structures remain accessible in ML_Root context;
2016-04-05 wenzelm 2016-04-05 clarified bootstrap environment;
2016-04-04 wenzelm 2016-04-04 option ML_system_unsafe;
2016-04-01 wenzelm 2016-04-01 lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
2016-04-01 wenzelm 2016-04-01 less bulky timing information, e.g. HOL 56913 ~> 672;
2016-04-01 wenzelm 2016-04-01 tuned whitespace;
2016-03-26 wenzelm 2016-03-26 avoid hardwired values;
2016-03-02 wenzelm 2016-03-02 support for ML_exception_debugger;
2016-02-25 wenzelm 2016-02-25 proper option process_output_tail, more generous default;
2016-01-10 wenzelm 2016-01-10 prune old versions more often, to reduce overall heap requirements;
2015-12-19 wenzelm 2015-12-19 prune old document versions more frequently, for reduced heap usage;
2015-11-09 wenzelm 2015-11-09 prefer explicit State panel;
2015-11-08 wenzelm 2015-11-08 added option timeout_scale;
2015-11-07 wenzelm 2015-11-07 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-02 wenzelm 2015-11-02 clarified completion of Isabelle symbols within document source;
2015-09-21 wenzelm 2015-09-21 option editor_output_state;
2015-09-11 wenzelm 2015-09-11 convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
2015-08-11 wenzelm 2015-08-11 init/exit depending on active debugger panels;
2015-08-10 wenzelm 2015-08-10 eliminated global option: breakpoints control this individually;
2015-08-05 wenzelm 2015-08-05 more controls;
2015-08-05 wenzelm 2015-08-05 tuned signature;
2015-07-21 wenzelm 2015-07-21 support for ML debugger;
2015-07-16 wenzelm 2015-07-16 added option ML_debugger;
2015-04-15 wenzelm 2015-04-15 GUI controls for ML_statistics, for more digestible protocol dump;
2015-01-29 wenzelm 2015-01-29 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;
2015-01-25 wenzelm 2015-01-25 discontinued obsolete option "document_graph";
2014-12-22 wenzelm 2014-12-22 system option "pretty_margin" is superseded by "thy_output_margin";
2014-10-31 wenzelm 2014-10-31 discontinued pointless option: timing is always on (overall theory only);
2014-08-13 wenzelm 2014-08-13 added option editor_syslog_limit;
2014-08-05 wenzelm 2014-08-05 added system option editor_output_delay: lower value might help big sessions under low-memory situations;
2014-05-06 wenzelm 2014-05-06 explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
2014-04-25 wenzelm 2014-04-25 suppress potential dangerous option (see 1baa5d19ac44);
2014-04-17 wenzelm 2014-04-17 tuned option name;
2014-03-25 wenzelm 2014-03-25 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);
2014-03-24 wenzelm 2014-03-24 discontinued Toplevel.debug in favour of system option "exception_trace";
2014-02-22 wenzelm 2014-02-22 support for completion within the formal context; tuned signature;
2013-08-25 wenzelm 2013-08-25 discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;
2013-07-31 wenzelm 2013-07-31 simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
2013-07-31 wenzelm 2013-07-31 simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
2013-07-30 wenzelm 2013-07-30 recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
2013-07-29 wenzelm 2013-07-29 NEWS; tuned description;
2013-07-29 wenzelm 2013-07-29 afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;
2013-07-29 wenzelm 2013-07-29 support declarative editor_execution_range, instead of old-style check/cancel buttons;
2013-07-27 wenzelm 2013-07-27 discontinued historic document formats;
2013-07-20 wenzelm 2013-07-20 option editor_execution_priority;
2013-07-20 wenzelm 2013-07-20 obscure options;
2013-07-19 wenzelm 2013-07-19 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);
2013-07-18 wenzelm 2013-07-18 proper system options for 'find_theorems';
2013-06-30 wenzelm 2013-06-30 tuned;
2013-06-30 wenzelm 2013-06-30 discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;
2013-05-18 wenzelm 2013-05-18 explicit notion of public options, which are shown in the editor options dialog; avoid hard-wired stuff;
2013-05-16 wenzelm 2013-05-16 more system options as context-sensitive config options;
2013-05-16 wenzelm 2013-05-16 Thy_Output.modes as proper option;
2013-05-13 wenzelm 2013-05-13 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
2013-05-13 wenzelm 2013-05-13 option "goals_limit", with more uniform description;
2013-03-27 wenzelm 2013-03-27 discontinued obsolete parallel_proofs_reuse_timing;
2013-03-27 wenzelm 2013-03-27 separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
2013-03-27 wenzelm 2013-03-27 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);
2013-03-13 wenzelm 2013-03-13 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
2013-02-20 wenzelm 2013-02-20 option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;