# HG changeset patch
# User wenzelm
# Date 1697014010 -7200
# Node ID f40b592922885308c54ba0f31b303efb78ee04d8
# Parent  019cec83b49f97fa1de0ca970218b016dc7f025d
clarified signature;

diff -r 019cec83b49f -r f40b59292288 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- 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 ()
diff -r 019cec83b49f -r f40b59292288 src/Pure/Concurrent/event_timer.ML
--- 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 =>
diff -r 019cec83b49f -r f40b59292288 src/Pure/Concurrent/future.ML
--- 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));
 
 
 
diff -r 019cec83b49f -r f40b59292288 src/Pure/Concurrent/isabelle_thread.ML
--- 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);
diff -r 019cec83b49f -r f40b59292288 src/Pure/System/message_channel.ML
--- 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;
diff -r 019cec83b49f -r f40b59292288 src/Pure/Tools/build.ML
--- 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