--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Wed Oct 11 10:16:17 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Wed Oct 11 10:46:50 2023 +0200
@@ -18,9 +18,6 @@
structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY =
struct
-fun make_thread interrupts body =
- 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
@@ -86,7 +83,7 @@
fun check_thread_manager () = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages} =>
if (case manager of SOME thread => Isabelle_Thread.is_active thread | NONE => false) then state
- else let val manager = SOME (make_thread false (fn () =>
+ else let val manager = SOME (Isabelle_Thread.fork (Isabelle_Thread.params "async_manager") (fn () =>
let
fun time_limit timeout_heap =
(case try Thread_Heap.min timeout_heap of
@@ -135,7 +132,7 @@
check_thread_manager ())
fun thread tool birth_time death_time desc f =
- (make_thread true
+ (Isabelle_Thread.fork (Isabelle_Thread.params "async_manager" |> Isabelle_Thread.interrupts)
(fn () =>
let
val self = Isabelle_Thread.self ()
--- a/src/Pure/Concurrent/event_timer.ML Wed Oct 11 10:16:17 2023 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Wed Oct 11 10:46:50 2023 +0200
@@ -129,9 +129,7 @@
fun manager_check 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);
+ else SOME (Isabelle_Thread.fork (Isabelle_Thread.params "event_timer") manager_loop);
fun shutdown () =
Thread_Attributes.uninterruptible_body (fn run =>
--- a/src/Pure/Concurrent/future.ML Wed Oct 11 10:16:17 2023 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Oct 11 10:46:50 2023 +0200
@@ -269,10 +269,7 @@
fun worker_start name = (*requires SYNCHRONIZED*)
let
- val worker =
- Isabelle_Thread.fork
- {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false}
- (fn () => worker_loop name);
+ val worker = Isabelle_Thread.fork (Isabelle_Thread.params "worker") (fn () => worker_loop name);
in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
@@ -380,10 +377,7 @@
fun scheduler_check () = (*requires SYNCHRONIZED*)
(do_shutdown := false;
if scheduler_active () then ()
- else
- scheduler :=
- SOME (Isabelle_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
- scheduler_loop));
+ else scheduler := SOME (Isabelle_Thread.fork (Isabelle_Thread.params "scheduler") scheduler_loop));
--- a/src/Pure/Concurrent/isabelle_thread.ML Wed Oct 11 10:16:17 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Wed Oct 11 10:46:50 2023 +0200
@@ -15,8 +15,11 @@
val self: unit -> T
val is_self: T -> bool
val threads_stack_limit: real Unsynchronized.ref
- val stack_limit: unit -> int option
- type params = {name: string, stack_limit: int option, interrupts: bool}
+ val default_stack_limit: unit -> int option
+ type params
+ val params: string -> params
+ val stack_limit: int -> params -> params
+ val interrupts: params -> params
val attributes: params -> Thread.Thread.threadAttribute list
val fork: params -> (unit -> unit) -> T
val is_active: T -> bool
@@ -81,24 +84,41 @@
val threads_stack_limit = Unsynchronized.ref 0.25;
-fun stack_limit () =
+fun default_stack_limit () =
let
val limit = Real.floor (! threads_stack_limit * 1024.0 * 1024.0 * 1024.0);
in if limit <= 0 then NONE else SOME limit end;
-type params = {name: string, stack_limit: int option, interrupts: bool};
+abstype params = Params of {name: string, stack_limit: int option, interrupts: bool}
+with
+
+fun make_params (name, stack_limit, interrupts) =
+ Params {name = name, stack_limit = stack_limit, interrupts = interrupts};
+
+fun params name = make_params (name, default_stack_limit (), false);
+fun stack_limit limit (Params {name, interrupts, ...}) = make_params (name, SOME limit, interrupts);
+fun interrupts (Params {name, stack_limit, ...}) = make_params (name, stack_limit, true);
-fun attributes ({stack_limit, interrupts, ...}: params) =
- Thread.Thread.MaximumMLStack stack_limit ::
+fun params_name (Params {name, ...}) = name;
+fun params_stack_limit (Params {stack_limit, ...}) = stack_limit;
+fun params_interrupts (Params {interrupts, ...}) = interrupts;
+
+end;
+
+fun attributes params =
+ Thread.Thread.MaximumMLStack (params_stack_limit params) ::
Thread_Attributes.convert_attributes
- (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
+ (if params_interrupts params
+ then Thread_Attributes.public_interrupts
+ else Thread_Attributes.no_interrupts);
-fun fork (params: params) body =
+fun fork params body =
let
val self = Single_Assignment.var "self";
fun main () =
let
- val t = init_self {thread = Thread.Thread.self (), name = #name params, id = make_id ()};
+ val name = params_name params;
+ val t = init_self {thread = Thread.Thread.self (), name = name, id = make_id ()};
val _ = Single_Assignment.assign self t;
in body () end;
val _ = Thread.Thread.fork (main, attributes params);
--- a/src/Pure/System/message_channel.ML Wed Oct 11 10:16:17 2023 +0200
+++ b/src/Pure/System/message_channel.ML Wed Oct 11 10:46:50 2023 +0200
@@ -38,8 +38,7 @@
| dispatch (Shutdown :: _) = ()
| dispatch (Message chunks :: rest) =
(Byte_Message.write_message_yxml stream chunks; dispatch rest);
- val thread =
- Isabelle_Thread.fork {name = "message_channel", stack_limit = NONE, interrupts = false} loop;
+ val thread = Isabelle_Thread.fork (Isabelle_Thread.params "message_channel") loop;
in Message_Channel {mbox = mbox, thread = thread} end;
end;
--- a/src/Pure/Tools/build.ML Wed Oct 11 10:16:17 2023 +0200
+++ b/src/Pure/Tools/build.ML Wed Oct 11 10:46:50 2023 +0200
@@ -102,9 +102,7 @@
fun exec e =
if can Theory.get_pure () then
- Isabelle_Thread.fork
- {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
- interrupts = false} e
+ Isabelle_Thread.fork (Isabelle_Thread.params "build_session") e
|> ignore
else e ();
in