# HG changeset patch
# User wenzelm
# Date 1697015220 -7200
# Node ID 96b3d13606b1c8917223017a3f275ea44934b162
# Parent  42e48ad59cda987ee896622253b3ea95b44108a9
proper Exn.capture;

diff -r 42e48ad59cda -r 96b3d13606b1 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 ());