src/Pure/PIDE/execution.ML
changeset 78757 a094bf81a496
parent 73101 3d5d949cd865
--- a/src/Pure/PIDE/execution.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/PIDE/execution.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -165,11 +165,11 @@
               val task = the (Future.worker_task ());
               val _ = status task [Markup.running];
               val result =
-                Exn.capture (Future.interruptible_task e) ()
+                Exn.capture_body (Future.interruptible_task e)
                 |> Future.identify_result pos
                 |> Exn.map_exn Runtime.thread_context;
               val errors =
-                Exn.capture (fn () =>
+                Exn.capture_body (fn () =>
                   (case result of
                     Exn.Exn exn =>
                      (status task [Markup.failed];
@@ -178,7 +178,7 @@
                       if exec_id = 0 then ()
                       else List.app (Future.error_message pos) (Runtime.exn_messages exn))
                   | Exn.Res _ =>
-                      status task [Markup.finished])) ();
+                      status task [Markup.finished]));
               val _ = status task [Markup.joined];
             in Exn.release errors; Exn.release result end);