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);
1.1 --- a/src/Pure/PIDE/execution.ML Mon Nov 25 18:03:38 2013 +0100
1.2 +++ b/src/Pure/PIDE/execution.ML Mon Nov 25 20:49:20 2013 +0100
1.3 @@ -104,17 +104,18 @@
1.4 val result =
1.5 Exn.capture (Future.interruptible_task e) ()
1.6 |> Future.identify_result pos;
1.7 - val _ = status task [Markup.finished, Markup.joined];
1.8 + val _ = status task [Markup.joined];
1.9 val _ =
1.10 (case result of
1.11 Exn.Res _ => ()
1.12 | Exn.Exn exn =>
1.13 - if exec_id = 0 orelse Exn.is_interrupt exn then ()
1.14 - else
1.15 - (status task [Markup.failed];
1.16 - Output.report (Markup.markup_only Markup.bad);
1.17 - List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
1.18 + (status task [Markup.failed];
1.19 + Output.report (Markup.markup_only Markup.bad);
1.20 + if exec_id = 0 then ()
1.21 + else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
1.22 + val _ = status task [Markup.finished];
1.23 in Exn.release result end);
1.24 +
1.25 val _ = status (Future.task_of future) [Markup.forked];
1.26 in future end)) ();
1.27