etc/options
9 months ago wenzelm 2018-10-02 unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
12 months ago wenzelm 2018-07-20 added system option "strict_facts";
12 months ago wenzelm 2018-06-24 disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
13 months ago wenzelm 2018-06-05 less wasteful consolidation, based on PIDE front-end state and recent changes;
13 months ago wenzelm 2018-06-02 less frequent consolidation: it requires a full Document.update and Document.start_execution;
14 months ago wenzelm 2018-05-19 support for build_database_server (PostgreSQL); clarified signature;
14 months ago wenzelm 2018-05-16 clarified "consolidation" vs. "presentation";
14 months ago wenzelm 2018-05-14 support for dynamic document output while editing;
14 months ago wenzelm 2018-05-11 some export of foundational theory content;
14 months ago wenzelm 2018-05-09 clarified future scheduling parameters, with support for parallel_limit;
16 months ago wenzelm 2018-03-02 avoid hardwired parameters; less ambitious defaults: low memory requirements;
18 months ago wenzelm 2018-01-25 more markup: disable spell-checker for raw latex;
18 months ago wenzelm 2018-01-09 more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
19 months ago wenzelm 2017-12-24 more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
19 months ago wenzelm 2017-12-13 positions as postlude: avoid intrusion of odd %-forms into main tex source;
19 months ago wenzelm 2017-12-12 option document_positions;
19 months ago wenzelm 2017-12-05 system option for default command tags;
19 months ago wenzelm 2017-12-05 tuned;
21 months ago wenzelm 2017-10-07 theory qualifier is always session name (see also 31e8a86971a8);
23 months ago wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-06-21 wenzelm 2017-06-21 tuned granularity of parallel tasks;
2017-06-21 wenzelm 2017-06-21 clarified modules;
2017-05-08 wenzelm 2017-05-08 simplified default;
2017-04-27 wenzelm 2017-04-27 support for database connection;
2017-04-10 wenzelm 2017-04-10 explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
2017-04-09 wenzelm 2017-04-09 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
2017-03-15 wenzelm 2017-03-15 dynamic session_options for tuning parameters and initial prover options;
2017-03-07 wenzelm 2017-03-07 clarified modules;
2017-02-27 wenzelm 2017-02-27 clarified defaults;
2016-11-24 wenzelm 2016-11-24 explicit option editor_generated_input_delay, which is more aggressive by default;
2016-10-20 wenzelm 2016-10-20 prevent sporadic disconnection;
2016-10-19 wenzelm 2016-10-19 added system option "profiling";
2016-10-10 wenzelm 2016-10-10 clarified treatment of options; more uniform channels;
2016-10-01 wenzelm 2016-10-01 options for process policy, notably for multiprocessor machines;
2016-09-08 wenzelm 2016-09-08 option "checkpoint" helps to fine-tune global heap space management;
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;