# HG changeset patch
# User wenzelm
# Date 1695670246 -7200
# Node ID 3a3a70d4d422c8117c486e45853dbe19ac3adab9
# Parent  27b2368ca69d01302214080934c8e02d409f7bbe
clarified order of modules: early access to interrupt management of Isabelle_Threads;

diff -r 27b2368ca69d -r 3a3a70d4d422 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 21:09:25 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Mon Sep 25 21:30:46 2023 +0200
@@ -14,6 +14,7 @@
   val print: T -> string
   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 attributes: params -> Thread.Thread.threadAttribute list
@@ -45,11 +46,11 @@
 val get_name = #name o dest;
 val get_id = #id o dest;
 
-val equal = Thread.Thread.equal o apply2 get_thread;
+fun equal (t1, t2) = Thread.Thread.equal (get_thread t1, get_thread t2);
 
 fun print t =
   (case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^
-    "-" ^ string_of_int (get_id t);
+    "-" ^ Int.toString (get_id t);
 
 
 (* self *)
@@ -75,11 +76,12 @@
 
 (* fork *)
 
+val threads_stack_limit = Unsynchronized.ref 0.25;
+
 fun stack_limit () =
   let
-    val threads_stack_limit =
-      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
-  in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end;
+    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};
 
diff -r 27b2368ca69d -r 3a3a70d4d422 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Sep 25 21:09:25 2023 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 25 21:30:46 2023 +0200
@@ -28,6 +28,8 @@
 ML_file "Concurrent/unsynchronized.ML";
 ML_file "Concurrent/synchronized.ML";
 ML_file "Concurrent/counter.ML";
+ML_file "Concurrent/single_assignment.ML";
+ML_file "Concurrent/isabelle_thread.ML";
 
 ML_file "ML/ml_heap.ML";
 ML_file "ML/ml_print_depth0.ML";
@@ -121,8 +123,6 @@
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
-ML_file "Concurrent/single_assignment.ML";
-ML_file "Concurrent/isabelle_thread.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";
diff -r 27b2368ca69d -r 3a3a70d4d422 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Sep 25 21:09:25 2023 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Sep 25 21:30:46 2023 +0200
@@ -197,6 +197,7 @@
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
+  Isabelle_Thread.threads_stack_limit := Options.default_real "threads_stack_limit";
   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;