more explicit type Isabelle_Thread.T;
total operation Isabelle_Thread.self: upgrade raw ML threads implicitly;

--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Wed Sep 06 14:09:27 2023 +0200
@@ -26,21 +26,21 @@
 
 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 =
@@ -85,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 =
@@ -96,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
@@ -138,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);
    ())

--- a/src/Pure/Concurrent/event_timer.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Wed Sep 06 14:09:27 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);

--- a/src/Pure/Concurrent/future.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Sep 06 14:09:27 2023 +0200
@@ -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])

--- a/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Wed Sep 06 14:09:27 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
+  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 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, 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.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.self (), name = "", id = make_id ()}
+      in set_self t; t end);
+
+fun is_self t = equal (t, self ());
 
 end;
 
@@ -58,19 +83,26 @@
     (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
 
 fun fork (params: params) body =
-  Thread.fork (fn () => (set_name (#name params); body ()), attributes params);
+  let
+    val name = #name params;
+    val id = make_id ();
+    fun main () = (set_self (make {thread = Thread.self (), name = name, id = id}); body ());
+    val 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.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.interrupt (get_thread t) handle Thread _ => ();
 
 end;

--- a/src/Pure/Concurrent/task_queue.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Sep 06 14:09:27 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;
 
@@ -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 ([], []);

--- a/src/Pure/Concurrent/timeout.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Wed Sep 06 14:09:27 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 =

--- a/src/Pure/System/message_channel.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/Pure/System/message_channel.ML	Wed Sep 06 14:09:27 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;

--- a/src/Pure/Tools/debugger.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/Pure/Tools/debugger.ML	Wed Sep 06 14:09:27 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;
@@ -250,7 +250,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 ()))));