# HG changeset patch # User wenzelm # Date 1694026288 -7200 # Node ID 47d0c333d155612015264984e14e91d269a7de9e # Parent d4600635581995a942f281ffa62cf1866eea56ff clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML; diff -r d46006355819 -r 47d0c333d155 src/Pure/Concurrent/future.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; diff -r d46006355819 -r 47d0c333d155 src/Pure/Concurrent/isabelle_thread.ML --- 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; diff -r d46006355819 -r 47d0c333d155 src/Pure/Concurrent/multithreading.ML --- 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; diff -r d46006355819 -r 47d0c333d155 src/Pure/Concurrent/single_assignment.ML --- 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; diff -r d46006355819 -r 47d0c333d155 src/Pure/Concurrent/synchronized.ML --- 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); diff -r d46006355819 -r 47d0c333d155 src/Pure/Concurrent/task_queue.ML --- 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 diff -r d46006355819 -r 47d0c333d155 src/Pure/ML/ml_init.ML --- 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; diff -r d46006355819 -r 47d0c333d155 src/Pure/Tools/debugger.ML --- 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; diff -r d46006355819 -r 47d0c333d155 src/Tools/Metis/PortableIsabelle.sml --- 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; diff -r d46006355819 -r 47d0c333d155 src/Tools/Metis/metis.ML --- 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;