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

--- a/src/Pure/PIDE/execution.ML	Mon Nov 25 18:03:38 2013 +0100
+++ b/src/Pure/PIDE/execution.ML	Mon Nov 25 20:49:20 2013 +0100
@@ -104,17 +104,18 @@
               val result =
                 Exn.capture (Future.interruptible_task e) ()
                 |> Future.identify_result pos;
-              val _ = status task [Markup.finished, Markup.joined];
+              val _ = status task [Markup.joined];
               val _ =
                 (case result of
                   Exn.Res _ => ()
                 | Exn.Exn exn =>
-                    if exec_id = 0 orelse Exn.is_interrupt exn then ()
-                    else
-                      (status task [Markup.failed];
-                       Output.report (Markup.markup_only Markup.bad);
-                       List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
+                   (status task [Markup.failed];
+                    Output.report (Markup.markup_only Markup.bad);
+                    if exec_id = 0 then ()
+                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
+              val _ = status task [Markup.finished];
             in Exn.release result end);
+
       val _ = status (Future.task_of future) [Markup.forked];
     in future end)) ();