# HG changeset patch
# User wenzelm
# Date 1694026305 -7200
# Node ID d17fcfd075c39b4374b628299e22de24667ac9b3
# Parent  de8081bc85a00f9920b49f7d3ddd85b0fa850980# Parent  47d0c333d155612015264984e14e91d269a7de9e
merged

diff -r de8081bc85a0 -r d17fcfd075c3 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -19,34 +19,28 @@
 struct
 
 fun make_thread interrupts body =
-  Thread.fork
-    (fn () =>
-      Runtime.debugging NONE body () handle exn =>
-        if Exn.is_interrupt exn then ()
-        else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
-      Isabelle_Thread.attributes
-        {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
+  Isabelle_Thread.fork {name = "async_manager", stack_limit = NONE, interrupts = interrupts} body;
 
 fun implode_message (workers, work) =
   space_implode " " (Try.serial_commas "and" workers) ^ work
 
 structure Thread_Heap = Heap
 (
-  type elem = Time.time * Thread.thread
+  type elem = Time.time * Isabelle_Thread.T
   fun ord ((a, _), (b, _)) = Time.compare (a, b)
 )
 
-fun lookup_thread xs = AList.lookup Thread.equal xs
-fun delete_thread xs = AList.delete Thread.equal xs
-fun update_thread xs = AList.update Thread.equal xs
+fun lookup_thread xs = AList.lookup Isabelle_Thread.equal xs
+fun delete_thread xs = AList.delete Isabelle_Thread.equal xs
+fun update_thread xs = AList.update Isabelle_Thread.equal xs
 
 type state =
-  {manager: Thread.thread option,
+  {manager: Isabelle_Thread.T option,
    timeout_heap: Thread_Heap.T,
    active:
-     (Thread.thread
+     (Isabelle_Thread.T
       * (string * Time.time * Time.time * (string * string))) list,
-   canceling:  (Thread.thread * (string * Time.time * (string * string))) list,
+   canceling:  (Isabelle_Thread.T * (string * Time.time * (string * string))) list,
    messages: (bool * (string * (string * string))) list}
 
 fun make_state manager timeout_heap active canceling messages : state =
@@ -91,7 +85,7 @@
 
 fun check_thread_manager () = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, canceling, messages} =>
-    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
+    if (case manager of SOME thread => Isabelle_Thread.is_active thread | NONE => false) then state
     else let val manager = SOME (make_thread false (fn () =>
       let
         fun time_limit timeout_heap =
@@ -102,14 +96,14 @@
         (*action: find threads whose timeout is reached, and interrupt canceling threads*)
         fun action {manager, timeout_heap, active, canceling, messages} =
           let val (timeout_threads, timeout_heap') =
-            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap
+            Thread_Heap.upto (Time.now (), Isabelle_Thread.self ()) timeout_heap
           in
             if null timeout_threads andalso null canceling then
               NONE
             else
               let
                 val _ = List.app (Isabelle_Thread.interrupt_unsynchronized o #1) canceling
-                val canceling' = filter (Thread.isActive 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
           end
@@ -144,7 +138,7 @@
   (make_thread true
        (fn () =>
            let
-             val self = Thread.self ()
+             val self = Isabelle_Thread.self ()
              val _ = register tool birth_time death_time desc self
            in unregister (f ()) self end);
    ())
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -92,7 +92,7 @@
 datatype status = Normal | Shutdown_Req | Shutdown_Ack;
 
 datatype state =
-  State of {requests: requests, status: status, manager: Thread.thread option};
+  State of {requests: requests, status: status, manager: Isabelle_Thread.T option};
 
 fun make_state (requests, status, manager) =
   State {requests = requests, status = status, manager = manager};
@@ -128,7 +128,7 @@
   then manager_loop () else ();
 
 fun manager_check manager =
-  if is_some manager andalso Thread.isActive (the manager) then manager
+  if is_some manager andalso Isabelle_Thread.is_active (the manager) then manager
   else
     SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
       manager_loop);
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -121,12 +121,12 @@
 
 (* synchronization *)
 
-val scheduler_event = ConditionVar.conditionVar ();
-val work_available = ConditionVar.conditionVar ();
-val work_finished = ConditionVar.conditionVar ();
+val scheduler_event = Thread.ConditionVar.conditionVar ();
+val work_available = Thread.ConditionVar.conditionVar ();
+val work_finished = Thread.ConditionVar.conditionVar ();
 
 local
-  val lock = Mutex.mutex ();
+  val lock = Thread.Mutex.mutex ();
 in
 
 fun SYNCHRONIZED name = Multithreading.synchronized name lock;
@@ -138,10 +138,10 @@
   Multithreading.sync_wait (SOME (Time.now () + timeout)) cond lock;
 
 fun signal cond = (*requires SYNCHRONIZED*)
-  ConditionVar.signal cond;
+  Thread.ConditionVar.signal cond;
 
 fun broadcast cond = (*requires SYNCHRONIZED*)
-  ConditionVar.broadcast cond;
+  Thread.ConditionVar.broadcast cond;
 
 end;
 
@@ -150,7 +150,7 @@
 
 val queue = Unsynchronized.ref Task_Queue.empty;
 val next = Unsynchronized.ref 0;
-val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
+val scheduler = Unsynchronized.ref (NONE: Isabelle_Thread.T option);
 val canceled = Unsynchronized.ref ([]: group list);
 val do_shutdown = Unsynchronized.ref false;
 val max_workers = Unsynchronized.ref 0;
@@ -161,7 +161,7 @@
 val next_round = seconds 0.05;
 
 datatype worker_state = Working | Waiting | Sleeping;
-val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list);
+val workers = Unsynchronized.ref ([]: (Isabelle_Thread.T * worker_state Unsynchronized.ref) list);
 
 fun count_workers state = (*requires SYNCHRONIZED*)
   fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
@@ -245,18 +245,19 @@
   in () end;
 
 fun worker_wait worker_state cond = (*requires SYNCHRONIZED*)
-  (case AList.lookup Thread.equal (! workers) (Thread.self ()) of
+  (case AList.lookup Isabelle_Thread.equal (! workers) (Isabelle_Thread.self ()) of
     SOME state => Unsynchronized.setmp state worker_state wait cond
   | NONE => wait cond);
 
 fun worker_next () = (*requires SYNCHRONIZED*)
   if length (! workers) > ! max_workers then
-    (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ()));
+    (Unsynchronized.change workers (AList.delete Isabelle_Thread.equal (Isabelle_Thread.self ()));
      signal work_available;
      NONE)
   else
     let val urgent_only = count_workers Working > ! max_active in
-      (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ()) urgent_only) of
+      (case Unsynchronized.change_result queue
+          (Task_Queue.dequeue (Isabelle_Thread.self ()) urgent_only) of
         NONE => (worker_wait Sleeping work_available; worker_next ())
       | some => (signal work_available; some))
     end;
@@ -297,10 +298,10 @@
       then ML_statistics () else ();
 
     val _ =
-      if not tick orelse forall (Thread.isActive o #1) (! workers) then ()
+      if not tick orelse forall (Isabelle_Thread.is_active o #1) (! workers) then ()
       else
         let
-          val (alive, dead) = List.partition (Thread.isActive o #1) (! workers);
+          val (alive, dead) = List.partition (Isabelle_Thread.is_active o #1) (! workers);
           val _ = workers := alive;
         in
           Multithreading.tracing 0 (fn () =>
@@ -374,7 +375,7 @@
   do (); last_round := Time.zeroTime);
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
-  (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
+  (case ! scheduler of NONE => false | SOME thread => Isabelle_Thread.is_active thread);
 
 fun scheduler_check () = (*requires SYNCHRONIZED*)
  (do_shutdown := false;
@@ -509,7 +510,8 @@
 fun join_next atts deps = (*requires SYNCHRONIZED*)
   if null deps then NONE
   else
-    (case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of
+    (case Unsynchronized.change_result queue
+        (Task_Queue.dequeue_deps (Isabelle_Thread.self ()) deps) of
       (NONE, []) => NONE
     | (NONE, deps') =>
        (worker_waiting deps' (fn () =>
@@ -571,7 +573,7 @@
       val (result, job) = future_job group orig_atts (fn () => f x);
       val task =
         SYNCHRONIZED "enroll" (fn () =>
-          Unsynchronized.change_result queue (Task_Queue.enroll (Thread.self ()) name group));
+          Unsynchronized.change_result queue (Task_Queue.enroll (Isabelle_Thread.self ()) name group));
       val _ = worker_exec (task, [job]);
     in
       (case Single_Assignment.peek result of
@@ -670,7 +672,7 @@
               val passive_job =
                 SYNCHRONIZED "fulfill_result" (fn () =>
                   Unsynchronized.change_result queue
-                    (Task_Queue.dequeue_passive (Thread.self ()) task));
+                    (Task_Queue.dequeue_passive (Isabelle_Thread.self ()) task));
             in
               (case passive_job of
                 SOME true => worker_exec (task, [job])
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -6,38 +6,63 @@
 
 signature ISABELLE_THREAD =
 sig
-  val is_self: Thread.thread -> bool
-  val get_name: unit -> string
+  type T
+  val get_thread: T -> Thread.Thread.thread
+  val get_name: T -> string
+  val get_id: T -> int
+  val equal: T * T -> bool
+  val print: T -> string
+  val self: unit -> T
+  val is_self: T -> bool
   val stack_limit: unit -> int option
   type params = {name: string, stack_limit: int option, interrupts: bool}
-  val attributes: params -> Thread.threadAttribute list
-  val fork: params -> (unit -> unit) -> Thread.thread
-  val join: Thread.thread -> unit
-  val interrupt_unsynchronized: Thread.thread -> unit
+  val attributes: params -> Thread.Thread.threadAttribute list
+  val fork: params -> (unit -> unit) -> T
+  val is_active: T -> bool
+  val join: T -> unit
+  val interrupt_unsynchronized: T -> unit
 end;
 
 structure Isabelle_Thread: ISABELLE_THREAD =
 struct
 
+(* abstract type *)
+
+abstype T = T of {thread: Thread.Thread.thread, name: string, id: int}
+with
+  val make = T;
+  fun dest (T args) = args;
+end;
+
+val get_thread = #thread o dest;
+val get_name = #name o dest;
+val get_id = #id o dest;
+
+val equal = Thread.Thread.equal o apply2 get_thread;
+
+fun print t =
+  (case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^
+    "-" ^ string_of_int (get_id t);
+
+
 (* self *)
 
-fun is_self thread = Thread.equal (Thread.self (), thread);
-
-
-(* unique name *)
+val make_id = Counter.make ();
 
 local
-  val name_var = Thread_Data.var () : string Thread_Data.var;
-  val count = Counter.make ();
+  val self_var = Thread_Data.var () : T Thread_Data.var;
 in
 
-fun get_name () =
-  (case Thread_Data.get name_var of
-    SOME name => name
-  | NONE => raise Fail "Isabelle-specific thread required");
+fun set_self t = Thread_Data.put self_var (SOME t);
 
-fun set_name base =
-  Thread_Data.put name_var (SOME ("Isabelle." ^ base ^ "-" ^ string_of_int (count ())));
+fun self () =
+  (case Thread_Data.get self_var of
+    SOME t => t
+  | NONE =>
+      let val t = make {thread = Thread.Thread.self (), name = "", id = make_id ()}
+      in set_self t; t end);
+
+fun is_self t = equal (t, self ());
 
 end;
 
@@ -53,28 +78,31 @@
 type params = {name: string, stack_limit: int option, interrupts: bool};
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
-  Thread.MaximumMLStack stack_limit ::
+  Thread.Thread.MaximumMLStack stack_limit ::
   Thread_Attributes.convert_attributes
     (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
 
 fun fork (params: params) body =
-  Thread.fork (fn () =>
-    Exn.trace General.exnMessage tracing (fn () =>
-      (set_name (#name params); body ())
-        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
-    attributes params);
+  let
+    val name = #name params;
+    val id = make_id ();
+    fun main () = (set_self (make {thread = Thread.Thread.self (), name = name, id = id}); body ());
+    val thread = Thread.Thread.fork (main, attributes params);
+  in make {thread = thread, name = name, id = id} end;
 
 
 (* join *)
 
-fun join thread =
-  while Thread.isActive thread
+val is_active = Thread.Thread.isActive o get_thread;
+
+fun join t =
+  while is_active t
   do OS.Process.sleep (seconds 0.1);
 
 
 (* interrupt *)
 
-fun interrupt_unsynchronized thread =
-  Thread.interrupt thread handle Thread _ => ();
+fun interrupt_unsynchronized t =
+  Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
 end;
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -9,11 +9,12 @@
   val max_threads: unit -> int
   val max_threads_update: int -> unit
   val parallel_proofs: int ref
-  val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
+  val sync_wait: Time.time option -> Thread.ConditionVar.conditionVar -> Thread.Mutex.mutex ->
+    bool Exn.result
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
-  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
+  val synchronized: string -> Thread.Mutex.mutex -> (unit -> 'a) -> 'a
 end;
 
 structure Multithreading: MULTITHREADING =
@@ -24,9 +25,9 @@
 local
 
 fun num_processors () =
-  (case Thread.numPhysicalProcessors () of
+  (case Thread.Thread.numPhysicalProcessors () of
     SOME n => n
-  | NONE => Thread.numProcessors ());
+  | NONE => Thread.Thread.numProcessors ());
 
 fun max_threads_result m =
   if Thread_Data.is_virtual then 1
@@ -55,8 +56,8 @@
     (Thread_Attributes.sync_interrupts (Thread_Attributes.get_attributes ()))
     (fn _ =>
       (case time of
-        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
-      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
+        SOME t => Exn.Res (Thread.ConditionVar.waitUntil (cond, lock, t))
+      | NONE => (Thread.ConditionVar.wait (cond, lock); Exn.Res true))
       handle exn => Exn.Exn exn);
 
 
@@ -86,24 +87,24 @@
     if ! trace > 0 then
       let
         val immediate =
-          if Mutex.trylock lock then true
+          if Thread.Mutex.trylock lock then true
           else
             let
               val _ = tracing 5 (fn () => name ^ ": locking ...");
               val timer = Timer.startRealTimer ();
-              val _ = Mutex.lock lock;
+              val _ = Thread.Mutex.lock lock;
               val time = Timer.checkRealTimer timer;
               val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
             in false end;
         val result = Exn.capture (restore_attributes e) ();
         val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
-        val _ = Mutex.unlock lock;
+        val _ = Thread.Mutex.unlock lock;
       in result end
     else
       let
-        val _ = Mutex.lock lock;
+        val _ = Thread.Mutex.lock lock;
         val result = Exn.capture (restore_attributes e) ();
-        val _ = Mutex.unlock lock;
+        val _ = Thread.Mutex.unlock lock;
       in result end) ());
 
 end;
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -18,10 +18,10 @@
 
 datatype 'a state =
     Set of 'a
-  | Unset of {lock: Mutex.mutex, cond: ConditionVar.conditionVar};
+  | Unset of {lock: Thread.Mutex.mutex, cond: Thread.ConditionVar.conditionVar};
 
 fun init_state () =
-  Unset {lock = Mutex.mutex (), cond = ConditionVar.conditionVar ()};
+  Unset {lock = Thread.Mutex.mutex (), cond = Thread.ConditionVar.conditionVar ()};
 
 abstype 'a var = Var of {name: string, state: 'a state Unsynchronized.ref}
 with
@@ -62,7 +62,8 @@
           Set _ => assign_fail name
         | Unset _ =>
             Thread_Attributes.uninterruptible (fn _ => fn () =>
-             (state := Set x; RunCall.clearMutableBit state; ConditionVar.broadcast cond)) ())));
+             (state := Set x; RunCall.clearMutableBit state;
+               Thread.ConditionVar.broadcast cond)) ())));
 
 end;
 
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -27,10 +27,10 @@
 
 datatype 'a state =
     Immutable of 'a
-  | Mutable of {lock: Mutex.mutex, cond: ConditionVar.conditionVar, content: 'a};
+  | Mutable of {lock: Thread.Mutex.mutex, cond: Thread.ConditionVar.conditionVar, content: 'a};
 
 fun init_state x =
-  Mutable {lock = Mutex.mutex (), cond = ConditionVar.conditionVar (), content = x};
+  Mutable {lock = Thread.Mutex.mutex (), cond = Thread.ConditionVar.conditionVar (), content = x};
 
 fun immutable_fail name = raise Fail ("Illegal access to immutable value " ^ name);
 
@@ -59,7 +59,7 @@
         | Mutable _ =>
             Thread_Attributes.uninterruptible (fn _ => fn () =>
              (state := Immutable x; RunCall.clearMutableBit state;
-               ConditionVar.broadcast cond)) ())));
+               Thread.ConditionVar.broadcast cond)) ())));
 
 
 (* synchronized access *)
@@ -83,7 +83,7 @@
                 | SOME (y, x') =>
                     Thread_Attributes.uninterruptible (fn _ => fn () =>
                       (state := Mutable {lock = lock, cond = cond, content = x'};
-                        ConditionVar.broadcast cond; SOME y)) ()));
+                        Thread.ConditionVar.broadcast cond; SOME y)) ()));
         in try_change () end));
 
 fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -35,16 +35,16 @@
   val all_passive: queue -> bool
   val total_jobs: queue -> int
   val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
-  val cancel: queue -> group -> Thread.thread list
-  val cancel_all: queue -> group list * Thread.thread list
+  val cancel: queue -> group -> Isabelle_Thread.T list
+  val cancel_all: queue -> group list * Isabelle_Thread.T list
   val finish: task -> queue -> bool * queue
-  val enroll: Thread.thread -> string -> group -> queue -> task * queue
+  val enroll: Isabelle_Thread.T -> string -> group -> queue -> task * queue
   val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue
   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
-  val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
-  val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
-  val dequeue_deps: Thread.thread -> task list -> queue ->
+  val dequeue_passive: Isabelle_Thread.T -> task -> queue -> bool option * queue
+  val dequeue: Isabelle_Thread.T -> bool -> queue -> (task * (bool -> bool) list) option * queue
+  val dequeue_deps: Isabelle_Thread.T -> task list -> queue ->
     (((task * (bool -> bool) list) option * task list) * queue)
 end;
 
@@ -88,7 +88,7 @@
   the_list (! status) @
     (case parent of NONE => [] | SOME group => group_status_unsynchronized group);
 
-val lock = Mutex.mutex ();
+val lock = Thread.Mutex.mutex ();
 fun SYNCHRONIZED e = Multithreading.synchronized "group_status" lock e;
 
 in
@@ -224,7 +224,7 @@
 
 datatype job =
   Job of (bool -> bool) list |
-  Running of Thread.thread |
+  Running of Isabelle_Thread.T |
   Passive of unit -> bool;
 
 type jobs = job Task_Graph.T;
@@ -299,7 +299,7 @@
     val _ = cancel_group group Exn.Interrupt;
     val running =
       Tasks.fold (fn task =>
-          (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I))
+          (case get_job jobs task of Running thread => insert Isabelle_Thread.equal thread | _ => I))
         (get_tasks groups (group_id group)) [];
   in running end;
 
@@ -311,7 +311,7 @@
         val _ = cancel_group group Exn.Interrupt;
       in
         (case job of
-          Running t => (insert eq_group group groups, insert Thread.equal t running)
+          Running t => (insert eq_group group groups, insert Isabelle_Thread.equal t running)
         | _ => (groups, running))
       end;
     val running = Task_Graph.fold cancel_job jobs ([], []);
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -35,7 +35,7 @@
   else
     Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
       let
-        val self = Thread.self ();
+        val self = Isabelle_Thread.self ();
         val start = Time.now ();
 
         val request =
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/ML/ml_init.ML
--- a/src/Pure/ML/ml_init.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/ML/ml_init.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -19,8 +19,6 @@
 
 val error_depth = PolyML.error_depth;
 
-open Thread;
-
 datatype illegal = Interrupt;
 
 structure Basic_Exn: BASIC_EXN = Exn;
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/ML/ml_pp.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -8,6 +8,11 @@
 struct
 
 val _ =
+  ML_system_pp (fn _ => fn _ => fn t =>
+    PolyML.PrettyString ("<thread " ^ quote (Isabelle_Thread.print t) ^
+      (if Isabelle_Thread.is_active t then "" else " (inactive)") ^ ">"));
+
+val _ =
   ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
 
 val _ =
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/ROOT.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -370,4 +370,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";
-
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/System/message_channel.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -17,7 +17,7 @@
 
 datatype message = Shutdown | Message of XML.body list;
 
-datatype T = Message_Channel of {mbox: message Mailbox.T, thread: Thread.thread};
+datatype T = Message_Channel of {mbox: message Mailbox.T, thread: Isabelle_Thread.T};
 
 fun shutdown (Message_Channel {mbox, thread}) =
  (Mailbox.send mbox Shutdown;
diff -r de8081bc85a0 -r d17fcfd075c3 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Pure/Tools/debugger.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -22,7 +22,7 @@
   if msg = "" then ()
   else
     Output.protocol_message
-      (Markup.debugger_output (Isabelle_Thread.get_name ()))
+      (Markup.debugger_output (Isabelle_Thread.print (Isabelle_Thread.self ())))
       [[XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]];
 
 val writeln_message = output_message Markup.writelnN;
@@ -87,7 +87,8 @@
 val is_debugging = not o null o get_debugging;
 
 fun with_debugging e =
-  Thread_Data.setmp debugging_var (SOME (PolyML.DebuggerInterface.debugState (Thread.self ()))) e ();
+  Thread_Data.setmp debugging_var
+    (SOME (PolyML.DebuggerInterface.debugState (Thread.Thread.self ()))) e ();
 
 fun the_debug_state thread_name index =
   (case get_debugging () of
@@ -110,7 +111,7 @@
 
 fun is_stepping () =
   let
-    val stack = PolyML.DebuggerInterface.debugState (Thread.self ());
+    val stack = PolyML.DebuggerInterface.debugState (Thread.Thread.self ());
     val Stepping (stepping, depth) = get_stepping ();
   in stepping andalso (depth < 0 orelse length stack <= depth) end;
 
@@ -250,7 +251,7 @@
         (SOME (fn (_, break) =>
           if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
           then
-            (case try Isabelle_Thread.get_name () of
+            (case try (Isabelle_Thread.print o Isabelle_Thread.self) () of
               SOME thread_name => debugger_loop thread_name
             | NONE => ())
           else ()))));
diff -r de8081bc85a0 -r d17fcfd075c3 src/Tools/Metis/PortableIsabelle.sml
--- a/src/Tools/Metis/PortableIsabelle.sml	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Tools/Metis/PortableIsabelle.sml	Wed Sep 06 20:51:45 2023 +0200
@@ -13,7 +13,7 @@
 fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
 
 local
-  val lock = Mutex.mutex ();
+  val lock = Thread.Mutex.mutex ();
 in
   fun critical e () = Multithreading.synchronized "metis" lock e
 end;
diff -r de8081bc85a0 -r d17fcfd075c3 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Tue Sep 05 15:23:50 2023 +0200
+++ b/src/Tools/Metis/metis.ML	Wed Sep 06 20:51:45 2023 +0200
@@ -154,7 +154,7 @@
 fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
 
 local
-  val lock = Mutex.mutex ();
+  val lock = Thread.Mutex.mutex ();
 in
   fun critical e () = Multithreading.synchronized "metis" lock e
 end;