diff -r 85efa3d01b16 -r a7e4b412cc7c src/Pure/Concurrent/isabelle_thread.ML --- 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);