diff -r e10ef4f9c848 -r c7b2697094ac src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Sun Sep 24 15:55:42 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 16:17:43 2023 +0200
@@ -24,6 +24,8 @@
   val interrupt_exn: 'a Exn.result
   val interrupt_self: unit -> 'a
   val interrupt_other: T -> unit
+  val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
+  val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a
   val try: (unit -> 'a) -> 'a option
   val can: (unit -> 'a) -> bool
 end;
@@ -117,6 +119,12 @@
 fun interrupt_other t =
   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;
+
+fun try_finally e f =
+  Exn.release (Exn.capture e () before f ());
+
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();