src/Pure/Concurrent/isabelle_thread.ML

   val join: T -> unit
   val interrupt: exn
   val interrupt_exn: 'a Exn.result
   val interrupt_self: unit -> 'a
   val interrupt_other: T -> unit
+  val expose_interrupt: unit -> unit  (*exception Interrupt*)
   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;

 fun interrupt_self () = raise interrupt;
 
 fun interrupt_other t =
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
+fun expose_interrupt () =
+  let
+    val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ());
+    val _ = Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
+    val test = Exn.capture Thread.Thread.testInterrupt ();
+    val _ = Thread_Attributes.set_attributes orig_atts;
+  in Exn.release test end;
+
 fun try_catch e f =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     restore_attributes e ()
       handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn) ();