# HG changeset patch
# User wenzelm
# Date 1535913458 -7200
# Node ID 8b98db8fd183121d4807ab78b9c13e35cfa4bd9f
# Parent  feb1b1b3c51fed22e00fec51297069a27178c950
clarified bracketing of messages: [forked [running finished] joined];

diff -r feb1b1b3c51f -r 8b98db8fd183 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Sun Sep 02 20:10:53 2018 +0200
+++ b/src/Pure/PIDE/execution.ML	Sun Sep 02 20:37:38 2018 +0200
@@ -168,18 +168,19 @@
                 Exn.capture (Future.interruptible_task e) ()
                 |> Future.identify_result pos
                 |> Exn.map_exn Runtime.thread_context;
+              val errors =
+                Exn.capture (fn () =>
+                  (case result of
+                    Exn.Exn exn =>
+                     (status task [Markup.failed];
+                      status task [Markup.finished];
+                      Output.report [Markup.markup_only (Markup.bad ())];
+                      if exec_id = 0 then ()
+                      else List.app (Future.error_message pos) (Runtime.exn_messages exn))
+                  | Exn.Res _ =>
+                      status task [Markup.finished])) ();
               val _ = status task [Markup.joined];
-              val _ =
-                (case result of
-                  Exn.Exn exn =>
-                   (status task [Markup.failed];
-                    status task [Markup.finished];
-                    Output.report [Markup.markup_only (Markup.bad ())];
-                    if exec_id = 0 then ()
-                    else List.app (Future.error_message pos) (Runtime.exn_messages exn))
-                | Exn.Res _ =>
-                    status task [Markup.finished])
-            in Exn.release result end);
+            in Exn.release errors; Exn.release result end);
 
       val _ = status (Future.task_of future) [Markup.forked];
     in future end)) ();