added system option "strict_facts";

disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;

less wasteful consolidation, based on PIDE front-end state and recent changes;

less frequent consolidation: it requires a full Document.update and Document.start_execution;

support for build_database_server (PostgreSQL);
clarified signature;

clarified "consolidation" vs. "presentation";

support for dynamic document output while editing;

some export of foundational theory content;

clarified future scheduling parameters, with support for parallel_limit;

avoid hardwired parameters;
less ambitious defaults: low memory requirements;

more markup: disable spell-checker for raw latex;

more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;

more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);

positions as postlude: avoid intrusion of odd %-forms into main tex source;

option document_positions;

system option for default command tags;

tuned;

theory qualifier is always session name (see also 31e8a86971a8);

maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);

tuned granularity of parallel tasks;

clarified modules;

simplified default;

support for database connection;

explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;

added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;

dynamic session_options for tuning parameters and initial prover options;

clarified modules;

clarified defaults;

explicit option editor_generated_input_delay, which is more aggressive by default;

prevent sporadic disconnection;

added system option "profiling";

clarified treatment of options;
more uniform channels;

options for process policy, notably for multiprocessor machines;

option "checkpoint" helps to fine-tune global heap space management;

simplified bootstrap: critical structures remain accessible in ML_Root context;

clarified bootstrap environment;

option ML_system_unsafe;

lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;

less bulky timing information, e.g. HOL 56913 ~> 672;

tuned whitespace;

avoid hardwired values;

support for ML_exception_debugger;

proper option process_output_tail, more generous default;

prune old versions more often, to reduce overall heap requirements;

prune old document versions more frequently, for reduced heap usage;

prefer explicit State panel;

added option timeout_scale;

clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);

clarified completion of Isabelle symbols within document source;

option editor_output_state;

convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;

init/exit depending on active debugger panels;

eliminated global option: breakpoints control this individually;

more controls;

tuned signature;

support for ML debugger;

added option ML_debugger;

GUI controls for ML_statistics, for more digestible protocol dump;

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;

discontinued obsolete option "document_graph";

system option "pretty_margin" is superseded by "thy_output_margin";

discontinued pointless option: timing is always on (overall theory only);

added option editor_syslog_limit;

added system option editor_output_delay: lower value might help big sessions under low-memory situations;

explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";

suppress potential dangerous option (see 1baa5d19ac44);

tuned option name;

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);

discontinued Toplevel.debug in favour of system option "exception_trace";

support for completion within the formal context;
tuned signature;

discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
simplified Goal.future_enabled;

simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;

simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);

recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;

NEWS;
tuned description;

afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;

support declarative editor_execution_range, instead of old-style check/cancel buttons;

discontinued historic document formats;

option editor_execution_priority;

obscure options;

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);

proper system options for 'find_theorems';

tuned;

discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
discontinued unused proofterms for FOL;

explicit notion of public options, which are shown in the editor options dialog;
avoid hard-wired stuff;

more system options as context-sensitive config options;

Thy_Output.modes as proper option;

limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);

option "goals_limit", with more uniform description;

discontinued obsolete parallel_proofs_reuse_timing;

separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;

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);

clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
clarified unknown timing vs. zero timing;
tuned;

option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;

more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);

always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;

improved Monitor_Dockable, based on ML_Statistics operations;
tuned signature;

smarter handling of tracing messages: prover process pauses and enters user dialog;

more generous tracing limit -- rescaled in MB;

some support for ML runtime statistics;

isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
always generate sty files, as before c5d0f19ef7cb;

more generous tracing_limit, with explicit system option;

Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;

more precise sections;

tuned;

more options;

some support to organize options in sections;

explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;

clarified format of etc/options: only declarations, not re-definitions;

timeout for session build job;
tuned error messages;

explicit option skip_proofs;

some description of main build options;

more build options;

more build options;

refined "document_dump_mode": "all", "tex+sty", "tex";

discontinued slightly odd "browser_info_remote" -- it could point to a completely different version of the Isabelle library;

more build options;

more build options;

added "document_dump_only" (cf. negated usedir -C);

further imitation of ISABELLE_USEDIR_OPTIONS via options;

added "browser_info_remote" (cf. usedir -P);

tuned options;

timing is command line options, not system option;

clarified document options;

pass build options to ML;
some imitation of usedir Session.init;

require explicit initialization of options;
more explicit Position operations;

some basic Isabelle options;