# HG changeset patch
# User wenzelm
# Date 1526059620 -7200
# Node ID a8f40dd73c6114230453ddcb5f0a3e3131cdd2af
# Parent  d23af2dbb4e76938b559b64452e955fdb7deb53d
slightly more ambitious parallelism (again);

diff -r d23af2dbb4e7 -r a8f40dd73c61 src/Pure/Concurrent/future.ML
--- 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 ());