src/Pure/PIDE/execution.ML
changeset 54678 87910da843d5
parent 54646 2b38549374ba
child 56291 e79f76a48449
     1.1 --- a/src/Pure/PIDE/execution.ML	Thu Dec 05 20:06:28 2013 +0100
     1.2 +++ b/src/Pure/PIDE/execution.ML	Thu Dec 05 20:22:53 2013 +0100
     1.3 @@ -107,13 +107,14 @@
     1.4                val _ = status task [Markup.joined];
     1.5                val _ =
     1.6                  (case result of
     1.7 -                  Exn.Res _ => ()
     1.8 -                | Exn.Exn exn =>
     1.9 +                  Exn.Exn exn =>
    1.10                     (status task [Markup.failed];
    1.11 +                    status task [Markup.finished];
    1.12                      Output.report (Markup.markup_only Markup.bad);
    1.13                      if exec_id = 0 then ()
    1.14 -                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
    1.15 -              val _ = status task [Markup.finished];
    1.16 +                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
    1.17 +                | Exn.Res _ =>
    1.18 +                    status task [Markup.finished])
    1.19              in Exn.release result end);
    1.20  
    1.21        val _ = status (Future.task_of future) [Markup.forked];