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;
authorwenzelm
Mon Nov 25 20:49:20 2013 +0100 (2013-11-25 ago)
changeset 546462b38549374ba
parent 54645 c19c83f49fa5
child 54647 7a8512d6206d
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);
src/Pure/PIDE/execution.ML
     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