--- a/src/Pure/Concurrent/future.ML Fri May 11 19:03:33 2018 +0200
+++ b/src/Pure/Concurrent/future.ML Fri May 11 19:27:00 2018 +0200
@@ -584,9 +584,11 @@
(* scheduling parameters *)
fun enabled () =
- Multithreading.max_threads () > 1 andalso
- let val lim = Options.default_int "parallel_limit"
- in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end;
+ let val threads = Multithreading.max_threads () in
+ threads > 1 andalso
+ let val lim = threads * Options.default_int "parallel_limit"
+ in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end
+ end;
val relevant = (fn [] => false | [_] => false | _ => enabled ());