--- a/src/Pure/Concurrent/multithreading.ML Mon Apr 23 21:57:15 2018 +0100
+++ b/src/Pure/Concurrent/multithreading.ML Tue Apr 24 11:03:51 2018 +0200
@@ -10,6 +10,8 @@
val max_threads_update: int -> unit
val enabled: unit -> bool
val relevant: 'a list -> bool
+ val parallel_proofs: int ref
+ val parallel_proofs_enabled: int -> bool
val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
val trace: int ref
val tracing: int -> (unit -> string) -> unit
@@ -47,6 +49,14 @@
end;
+(* parallel_proofs *)
+
+val parallel_proofs = ref 1;
+
+fun parallel_proofs_enabled n =
+ enabled () andalso ! parallel_proofs >= n;
+
+
(* synchronous wait *)
fun sync_wait time cond lock =