src/Pure/PIDE/execution.ML
2013-12-05 wenzelm 2013-12-05 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash; tuned signature;
2013-11-25 wenzelm 2013-11-25 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);
2013-09-03 wenzelm 2013-09-03 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);
2013-08-25 wenzelm 2013-08-25 tuned;
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;
2013-07-30 wenzelm 2013-07-30 pro-forma Execution.reset, despite lack of final join/commit;
2013-07-30 wenzelm 2013-07-30 de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
2013-07-29 wenzelm 2013-07-29 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;
2013-07-29 wenzelm 2013-07-29 obsolete;
2013-07-15 wenzelm 2013-07-15 more careful termination of removed execs, leaving running execs undisturbed;
2013-07-12 wenzelm 2013-07-12 tuned;
2013-07-12 wenzelm 2013-07-12 clarified execution: maintain running execs only, check "stable" separately via memo (again); tuned signatures;
2013-07-12 wenzelm 2013-07-12 tuned signature; tuned comments;
2013-07-12 wenzelm 2013-07-12 clarified module name;