more robust;

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

Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
tuned;

tuned;

tuned signature;

tuned -- use XZ.Cache;

more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
tuned;

store exports within PIDE command state;
Markup.Export.unapply: proper NAME;

protocol message for export of theory resources;

update XML cache for slightly modified messages;

provide theory timing information, similar to command timing but always considered relevant;

tuned signature;

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

more general dispatcher operations;

global session_base for PIDE interaction;

tuned signature;

more informative session result;

clarified signature;

more realistic PIDE build session;

asynchronous send_stop operation;

dynamic session_options for tuning parameters and initial prover options;

more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;

more robust debugger initialization, e.g. required for GUI components before actual session startup;

more abstract module Document;

misc tuning and simplification;

more explicit Session.xml_cache;

tuned signature;

clarified modules;

proper local debugger state, depending on session;
tuned signature;

tuned signature;

more robust Session.stop: idempotent, avoid conflict with startup;

more strict Session.start: no restart from terminated session;

clarified Session.Phase;

tuned signature;

uniform Document.Model.node_edits (without void edits);

emit Commands_Changed for blobs as well, e.g. relevant for isabelle.vscode.Server.prover_output;

tuned signature -- prover-independence is presently theoretical;

more abstract Session.start, without prover command-line;
Isabelle_Process.apply is directly based on ML_Process;
clarified Isabelle_Process.main command-line;
tuned signature;

Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
more robust File.bash_escape;
more robust treatment of ML_OPTIONS;
clarified prover args (again);

clarified bash process -- similar to ML version;

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

clarified order of shutdown;

tuned;

clarified modules;

--HG--
rename : src/Pure/Concurrent/simple_thread.ML => src/Pure/Concurrent/standard_thread.ML
rename : src/Pure/Concurrent/simple_thread.scala => src/Pure/Concurrent/standard_thread.scala

more explicit HTML.symbols;
tuned signature;

output HTML text according to Isabelle/Scala Symbol.Interpretation;

tuned;

tuned signature;

clarified management of (single) session;
proper Debugger.Update events;

skeleton for interactive debugger;

obsolete (see also 94b2690ad494);

more type-safe handler interface;
proper progress for Build.Handler;

clarified build_theories: proper protocol handler;

clarified build_theories;

some support for PIDE batch session;
clarified Thy_Info.use_thys_options and corresponding protocol command;

tuned;

node-specific keywords, with session base syntax as default;

node-specific syntax, with base_syntax as default;
clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;

tuned comments;

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

obsolete (see f7700146678d);

more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);

less warnings -- ignore potential prover startup/shutdown races;

support print operations as asynchronous query;

tuned;

more synchronized treatment of prover process, which might emit more messages before shutdown and requires manager to accept them;

more systematic Isabelle output, like in classic Isabelle/ML (without markup);

improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;

tuned comments;

more systematic delay_first discipline for change_buffer and prune_history;

tuned -- potentially more robust;

manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);

simplified change_buffer (again, see 937826d702d5): no thread, just timer, rely on asynchronous commands_changed.post;

clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;

more robust prover termination;

more explicit checks;

tuned signature;

more uniform warning/error handling, potentially with propagation to send_wait caller;

more careful shutdown (amending f2f53f7046f4);

converted main session manager to Consumer_Thread: messages need to be consumed immediately, postponed_changes replaces implicit actor mailbox scanning;

simplified commands_changed_buffer (in contrast to a8331fb5c959): rely on better performance of Consumer_Thread/Mailbox and more direct Timer (like session_actor.receiver);

simplified -- prefer Consumer_Thread over Actor;

tuned signature, in accordance to ML version;

eliminated redundant Volatile;

tuned signature in accordance to ML version;

explicit Exn.error_message in accordance to Output.error_message in ML;

more permissive Session.update_options: this is wired to jEdit PropertiesChanged, which may occur before the prover is started;

clarified Version.syntax -- avoid guessing initial situation;

more abstract Prover.Syntax, as proposed by Carst Tankink;

more general prover operations;

more general prover operations;

store blob content within document node: aux. files that were once open are made persistent;
proper structural equality for Command.File and Symbol.Index;

propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
tuned signature;

tuned signature;

clarified module arrangement;

--HG--
rename : src/Pure/System/session.ML => src/Pure/PIDE/session.ML
rename : src/Pure/System/session.scala => src/Pure/PIDE/session.scala