--- 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 ();