src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed May 09 20:45:57 2018 +0200
@@ -34,6 +34,10 @@
   val forked_results: {name: string, deps: Task_Queue.task list} ->
     (unit -> 'a) list -> 'a Exn.result list
   val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b
+  val enabled: unit -> bool
+  val relevant: 'a list -> bool
+  val proofs_enabled: int -> bool
+  val proofs_enabled_timing: Time.time -> bool
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
   val cond_forks: params -> (unit -> 'a) list -> 'a future list
@@ -577,6 +581,22 @@
     end);
 
 
+(* 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;
+
+val relevant = (fn [] => false | [_] => false | _ => enabled ());
+
+fun proofs_enabled n =
+  ! Multithreading.parallel_proofs >= n andalso is_some (worker_task ()) andalso enabled ();
+
+fun proofs_enabled_timing t =
+  proofs_enabled 1 andalso Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
+
+
 (* fast-path operations -- bypass task queue if possible *)
 
 fun value_result (res: 'a Exn.result) =
@@ -590,7 +610,7 @@
 fun value x = value_result (Exn.Res x);
 
 fun cond_forks args es =
-  if Multithreading.enabled () then forks args es
+  if enabled () then forks args es
   else map (fn e => value_result (Exn.interruptible_capture e ())) es;
 
 fun map_future f x =