src/Pure/PIDE/execution.ML
Wed, 26 Mar 2014 20:32:15 +0100 wenzelm support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
Wed, 26 Mar 2014 20:08:07 +0100 wenzelm less markup by default -- this is stored persistently in Isabelle/Scala;
Wed, 26 Mar 2014 12:32:51 +0100 wenzelm more uniform Execution.fork vs. Execution.print;
Wed, 26 Mar 2014 12:15:42 +0100 wenzelm added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
Thu, 05 Dec 2013 20:22:53 +0100 wenzelm more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
Mon, 25 Nov 2013 20:49:20 +0100 wenzelm 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;
Tue, 03 Sep 2013 11:29:01 +0200 wenzelm Execution.fork formally requires registered Execution.running;
Sun, 25 Aug 2013 20:43:10 +0200 wenzelm tuned;
Sun, 25 Aug 2013 20:32:26 +0200 wenzelm maintain goal forks as part of global execution;
Tue, 30 Jul 2013 12:07:14 +0200 wenzelm pro-forma Execution.reset, despite lack of final join/commit;
Tue, 30 Jul 2013 11:38:43 +0200 wenzelm de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
Mon, 29 Jul 2013 18:59:58 +0200 wenzelm keep memo_exec execution running, which is important to cancel goal forks eventually;
Mon, 29 Jul 2013 13:00:36 +0200 wenzelm obsolete;
Mon, 15 Jul 2013 10:25:35 +0200 wenzelm more careful termination of removed execs, leaving running execs undisturbed;
Fri, 12 Jul 2013 12:17:03 +0200 wenzelm tuned;
Fri, 12 Jul 2013 12:04:16 +0200 wenzelm clarified execution: maintain running execs only, check "stable" separately via memo (again);
Fri, 12 Jul 2013 11:28:03 +0200 wenzelm tuned signature;
Fri, 12 Jul 2013 11:07:02 +0200 wenzelm clarified module name;
less more (0) tip