src/Pure/Concurrent/isabelle_thread.ML
changeset 78787 a7e4b412cc7c
parent 78786 85efa3d01b16
--- a/src/Pure/Concurrent/isabelle_thread.ML	Tue Oct 17 11:52:52 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Tue Oct 17 12:10:58 2023 +0200
@@ -26,8 +26,8 @@
   val join: T -> unit
   val interrupt: exn
   val interrupt_exn: 'a Exn.result
-  val interrupt_self: unit -> 'a
-  val interrupt_other: T -> unit
+  val raise_interrupt: unit -> 'a
+  val interrupt_thread: T -> unit
   structure Exn: EXN
   val expose_interrupt_result: unit -> unit Exn.result
   val expose_interrupt: unit -> unit  (*exception Exn.is_interrupt*)
@@ -140,9 +140,9 @@
 val interrupt = Exn.Interrupt_Break;
 val interrupt_exn = Exn.Exn interrupt;
 
-fun interrupt_self () = raise interrupt;
+fun raise_interrupt () = raise interrupt;
 
-fun interrupt_other t =
+fun interrupt_thread t =
   Synchronized.change (#break (dest t))
     (fn b => (Thread.Thread.interrupt (get_thread t); true) handle Thread.Thread _ => b);