# HG changeset patch
# User wenzelm
# Date 1697536372 -7200
# Node ID 85efa3d01b1603195b6a2189fe3ebd6f50f0f86e
# Parent  c8202ed06a5c2b2cec62d233802dd3879a0fb5e4
more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;

diff -r c8202ed06a5c -r 85efa3d01b16 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Tue Oct 17 11:47:13 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Tue Oct 17 11:52:52 2023 +0200
@@ -170,9 +170,10 @@
     fun main () =
       (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
        Thread.Thread.testInterrupt ());
-    val test = check_interrupt_exn (Exn.capture_body main);
+    val test = Exn.capture0 main ();
     val _ = Thread_Attributes.set_attributes orig_atts;
-  in test end;
+    val break = reset_interrupt ();
+  in if Exn.is_interrupt_exn test then Exn.Exn (make_interrupt break) else test end;
 
 val expose_interrupt = Exn.release o expose_interrupt_result;