more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;
authorwenzelm
Tue, 17 Oct 2023 11:52:52 +0200
changeset 78786 85efa3d01b16
parent 78785 c8202ed06a5c
child 78787 a7e4b412cc7c
more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;
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;