slightly more ambitious parallelism (again);
authorwenzelm
Fri, 11 May 2018 19:27:00 +0200
changeset 68147 a8f40dd73c61
parent 68146 d23af2dbb4e7
child 68148 fb661e4c4717
slightly more ambitious parallelism (again);
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 ());