--- a/src/Pure/Concurrent/future.ML Sun May 24 20:35:24 2020 +0200
+++ b/src/Pure/Concurrent/future.ML Sun May 24 20:59:34 2020 +0200
@@ -276,11 +276,9 @@
fun worker_start name = (*requires SYNCHRONIZED*)
let
- val threads_stack_limit =
- Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
- val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
val worker =
- Isabelle_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+ Isabelle_Thread.fork
+ {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false}
(fn () => worker_loop name);
in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
--- a/src/Pure/Concurrent/isabelle_thread.ML Sun May 24 20:35:24 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Sun May 24 20:59:34 2020 +0200
@@ -8,6 +8,7 @@
sig
val is_self: Thread.thread -> bool
val get_name: unit -> string
+ 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
@@ -43,6 +44,12 @@
(* fork *)
+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;
+
type params = {name: string, stack_limit: int option, interrupts: bool};
fun attributes ({stack_limit, interrupts, ...}: params) =