# HG changeset patch
# User wenzelm
# Date 1695656272 -7200
# Node ID b54aee45cabe3a3bf10e19ef6cf2db080c4e4aad
# Parent  55b1664b564be497f86c51184496acd46595267d
more robust: catch/finally part is uninterruptible;

diff -r 55b1664b564b -r b54aee45cabe src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 17:37:12 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 17:37:52 2023 +0200
@@ -120,10 +120,13 @@
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
 fun try_catch e f =
-  e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn;
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+    restore_attributes e ()
+      handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn) ();
 
 fun try_finally e f =
-  Exn.release (Exn.capture e () before f ());
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+    Exn.release (Exn.capture (restore_attributes e) () before f ())) ();
 
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();