clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;

--- a/src/Pure/Concurrent/future.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Sep 06 20:51:28 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;
 

--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Wed Sep 06 20:51:28 2023 +0200
@@ -7,7 +7,7 @@
 signature ISABELLE_THREAD =
 sig
   type T
-  val get_thread: T -> Thread.thread
+  val get_thread: T -> Thread.Thread.thread
   val get_name: T -> string
   val get_id: T -> int
   val equal: T * T -> bool
@@ -16,7 +16,7 @@
   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 attributes: params -> Thread.Thread.threadAttribute list
   val fork: params -> (unit -> unit) -> T
   val is_active: T -> bool
   val join: T -> unit
@@ -28,7 +28,7 @@
 
 (* abstract type *)
 
-abstype T = T of {thread: Thread.thread, name: string, id: int}
+abstype T = T of {thread: Thread.Thread.thread, name: string, id: int}
 with
   val make = T;
   fun dest (T args) = args;
@@ -38,7 +38,7 @@
 val get_name = #name o dest;
 val get_id = #id o dest;
 
-val equal = Thread.equal o apply2 get_thread;
+val equal = Thread.Thread.equal o apply2 get_thread;
 
 fun print t =
   (case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^
@@ -59,7 +59,7 @@
   (case Thread_Data.get self_var of
     SOME t => t
   | NONE =>
-      let val t = make {thread = Thread.self (), name = "", id = make_id ()}
+      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 ());
@@ -78,7 +78,7 @@
 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);
 
@@ -86,14 +86,14 @@
   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);
+    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 *)
 
-val is_active = Thread.isActive o get_thread;
+val is_active = Thread.Thread.isActive o get_thread;
 
 fun join t =
   while is_active t
@@ -103,6 +103,6 @@
 (* interrupt *)
 
 fun interrupt_unsynchronized t =
-  Thread.interrupt (get_thread t) handle Thread _ => ();
+  Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
 end;

--- a/src/Pure/Concurrent/multithreading.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Wed Sep 06 20:51:28 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;

--- a/src/Pure/Concurrent/single_assignment.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Wed Sep 06 20:51:28 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;
 

--- a/src/Pure/Concurrent/synchronized.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Wed Sep 06 20:51:28 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);

--- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Sep 06 20:51:28 2023 +0200
@@ -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

--- a/src/Pure/ML/ml_init.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/ML/ml_init.ML	Wed Sep 06 20:51:28 2023 +0200
@@ -19,8 +19,6 @@
 
 val error_depth = PolyML.error_depth;
 
-open Thread;
-
 datatype illegal = Interrupt;
 
 structure Basic_Exn: BASIC_EXN = Exn;

--- a/src/Pure/Tools/debugger.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Pure/Tools/debugger.ML	Wed Sep 06 20:51:28 2023 +0200
@@ -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;
 

--- a/src/Tools/Metis/PortableIsabelle.sml	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Tools/Metis/PortableIsabelle.sml	Wed Sep 06 20:51:28 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;

--- a/src/Tools/Metis/metis.ML	Wed Sep 06 16:03:22 2023 +0200
+++ b/src/Tools/Metis/metis.ML	Wed Sep 06 20:51:28 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;