tuned signature -- prefer bulk messages;

clarified bracketing of messages: [forked [running finished] joined];

tuned;

record active execution task and depend on it -- avoid new executions bumping into old ones;

tuned -- more explicit types;

clarified future scheduling parameters, with support for parallel_limit;

clarified signature;

clarified signature;

more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;

more synchronized Execution.snapshot;

clarified build errors;
tuned signature;

more uniform treatment of "bad" like other messages (with serial number);

clarified bootstrap;

tuned signature;

thread context for exceptions from forks, e.g. relevant when printing errors;
tuned signature;

unused;

do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);

support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;

tuned;

redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
more explicit ML_Compiler.flags;

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);

less markup by default -- this is stored persistently in Isabelle/Scala;
removed dead code;

more uniform Execution.fork vs. Execution.print;
asynchronous Execution.fork_prints, entrusted to Execution.fork management (NB: Command.print_finished is only relevant for persistent print functions);

added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
misc tuning;

more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
tuned signature;

more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
more defensive order of Markup.failed vs. Markup.finished, to allow breakdown of ML execution context (see also d7a1973b063c);

Execution.fork formally requires registered Execution.running;
Thy_Info.load_thy: more official exec_id registration (batch mode);
dummy exec Document_ID.none is always registered (TTY mode);
clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);

tuned;

maintain goal forks as part of global execution;
tuned;

pro-forma Execution.reset, despite lack of final join/commit;

de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;

keep memo_exec execution running, which is important to cancel goal forks eventually;
run as nested worker task to keep main group valid, even after cancelation of removed subgroups;
do not memoize interrupt, but absorb it silently in main execution;
Goal.purge_futures: rough sanity check of group status;

obsolete;

more careful termination of removed execs, leaving running execs undisturbed;

tuned;

clarified execution: maintain running execs only, check "stable" separately via memo (again);
tuned signatures;

tuned signature;
tuned comments;

clarified module name;

--HG--
rename : src/Pure/PIDE/exec.ML => src/Pure/PIDE/execution.ML