proper Exn.capture;
authorwenzelm
Wed, 11 Oct 2023 11:07:00 +0200
changeset 78756 96b3d13606b1
parent 78755 42e48ad59cda
child 78757 a094bf81a496
proper Exn.capture;
src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Wed Oct 11 11:06:34 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Wed Oct 11 11:07:00 2023 +0200
@@ -139,14 +139,17 @@
         raise Fail "Concurrent attempt to shutdown event timer"
       else (true, make_state (requests, Shutdown_Req, manager_check manager)))
     then
-      run (fn () =>
-        Synchronized.guarded_access state
-          (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) ()
-      handle exn =>
-        if Exn.is_interrupt exn then
+      let
+        fun main () =
+          Synchronized.guarded_access state
+            (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE);
+        val result = Exn.capture (run main) ();
+      in
+        if Exn.is_interrupt_exn result then
           Synchronized.change state (fn State {requests, manager, ...} =>
             make_state (requests, Normal, manager))
-        else ()
+        else Exn.release result
+      end
     else ());