# HG changeset patch
# User wenzelm
# Date 1697536033 -7200
# Node ID c8202ed06a5c2b2cec62d233802dd3879a0fb5e4
# Parent  fb46520b9b7c0d95aa57b549563f056b0dea5142
tuned;

diff -r fb46520b9b7c -r c8202ed06a5c src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Mon Oct 16 21:27:56 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Tue Oct 17 11:47:13 2023 +0200
@@ -146,13 +146,13 @@
   Synchronized.change (#break (dest t))
     (fn b => (Thread.Thread.interrupt (get_thread t); true) handle Thread.Thread _ => b);
 
+fun reset_interrupt () =
+  Synchronized.change_result (#break (dest (self ()))) (fn b => (b, false));
+
+fun make_interrupt break = if break then Exn.Interrupt_Break else Exn.Interrupt_Breakdown;
+
 fun check_interrupt exn =
-  if Exn.is_interrupt_raw exn then
-    let
-      val t = self ();
-      val break = Synchronized.change_result (#break (dest t)) (fn b => (b, false));
-    in if break then Exn.Interrupt_Break else Exn.Interrupt_Breakdown end
-  else exn;
+  if Exn.is_interrupt_raw exn then make_interrupt (reset_interrupt ()) else exn;
 
 fun check_interrupt_exn result =
   Exn.map_exn check_interrupt result;