--- 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);
())
--- 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);
--- 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])
--- 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;
--- 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;
--- 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;
--- 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);
--- 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 ([], []);
--- 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 =
--- 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;
--- 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 _ =
--- 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";
-
--- 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;
--- 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 ()))));
--- 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;
--- 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;