# HG changeset patch
# User wenzelm
# Date 1697537458 -7200
# Node ID a7e4b412cc7c625d9bdb9e726fe8b1dae41f9955
# Parent  85efa3d01b1603195b6a2189fe3ebd6f50f0f86e
tuned signature, following Isabelle/Scala;

diff -r 85efa3d01b16 -r a7e4b412cc7c src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 17 11:52:52 2023 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 17 12:10:58 2023 +0200
@@ -1051,7 +1051,7 @@
       in
         if not (null ps) orelse rc = 0 then Normal (ps, js, first_error)
         else if rc = 2 then TimedOut js
-        else if rc = 130 then Isabelle_Thread.interrupt_self ()
+        else if rc = 130 then Isabelle_Thread.raise_interrupt ()
         else Error (if first_error = "" then "Unknown error" else first_error, js)
       end
   end
diff -r 85efa3d01b16 -r a7e4b412cc7c src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Oct 17 11:52:52 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Oct 17 12:10:58 2023 +0200
@@ -99,7 +99,7 @@
               NONE
             else
               let
-                val _ = List.app (Isabelle_Thread.interrupt_other o #1) canceling
+                val _ = List.app (Isabelle_Thread.interrupt_thread o #1) canceling
                 val canceling' = filter (Isabelle_Thread.is_active o #1) canceling
                 val state' = make_state manager timeout_heap' active canceling' messages
               in SOME (map #2 timeout_threads, state') end
diff -r 85efa3d01b16 -r a7e4b412cc7c src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Oct 17 11:52:52 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Oct 17 12:10:58 2023 +0200
@@ -195,13 +195,13 @@
     val running = Task_Queue.cancel (! queue) group;
     val _ = running |> List.app (fn thread =>
       if Isabelle_Thread.is_self thread then ()
-      else Isabelle_Thread.interrupt_other thread);
+      else Isabelle_Thread.interrupt_thread thread);
   in running end;
 
 fun cancel_all () = (*requires SYNCHRONIZED*)
   let
     val (groups, threads) = Task_Queue.cancel_all (! queue);
-    val _ = List.app Isabelle_Thread.interrupt_other threads;
+    val _ = List.app Isabelle_Thread.interrupt_thread threads;
   in groups end;
 
 fun cancel_later group = (*requires SYNCHRONIZED*)
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);
 
diff -r 85efa3d01b16 -r a7e4b412cc7c src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Tue Oct 17 11:52:52 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Tue Oct 17 12:10:58 2023 +0200
@@ -40,7 +40,7 @@
 
         val request =
           Event_Timer.request {physical = physical} (start + scale_time timeout)
-            (fn () => Isabelle_Thread.interrupt_other self);
+            (fn () => Isabelle_Thread.interrupt_thread self);
         val result =
           Exn.capture_body (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x));
 
diff -r 85efa3d01b16 -r a7e4b412cc7c src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Oct 17 11:52:52 2023 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Oct 17 12:10:58 2023 +0200
@@ -244,7 +244,7 @@
           val _ = status tr Markup.failed;
           val _ = status tr Markup.finished;
           val _ =
-            if null errs then (status tr Markup.canceled; Isabelle_Thread.interrupt_self ())
+            if null errs then (status tr Markup.canceled; Isabelle_Thread.raise_interrupt ())
             else ();
         in {failed = true, command = tr, state = st} end
     | SOME st' =>
diff -r 85efa3d01b16 -r a7e4b412cc7c src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Tue Oct 17 11:52:52 2023 +0200
+++ b/src/Pure/System/isabelle_system.ML	Tue Oct 17 12:10:58 2023 +0200
@@ -68,7 +68,7 @@
               if head = Bash.server_uuid andalso length args = 1 then
                 loop (SOME (hd args)) s
               else if head = Bash.server_interrupt andalso null args then
-                Isabelle_Thread.interrupt_self ()
+                Isabelle_Thread.raise_interrupt ()
               else if head = Bash.server_failure andalso length args = 1 then
                 raise Fail (hd args)
               else if head = Bash.server_result andalso length args >= 4 then