src/Pure/goal.ML
changeset 32061 11f8ee55662d
parent 32058 c76fd93b3b99
child 32062 457f5bcd3d76
     1.1 --- a/src/Pure/goal.ML	Sun Jul 19 19:20:17 2009 +0200
     1.2 +++ b/src/Pure/goal.ML	Sun Jul 19 19:24:04 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature BASIC_GOAL =
     1.6  sig
     1.7 -  val parallel_proofs: bool ref
     1.8 +  val parallel_proofs: int ref
     1.9    val SELECT_GOAL: tactic -> int -> tactic
    1.10    val CONJUNCTS: tactic -> int -> tactic
    1.11    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    1.12 @@ -21,6 +21,7 @@
    1.13    val finish: thm -> thm
    1.14    val norm_result: thm -> thm
    1.15    val future_enabled: unit -> bool
    1.16 +  val local_future_enabled: unit -> bool
    1.17    val future_result: Proof.context -> thm future -> term -> thm
    1.18    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.19    val prove_multi: Proof.context -> string list -> term list -> term list ->
    1.20 @@ -95,10 +96,12 @@
    1.21  
    1.22  (* future_enabled *)
    1.23  
    1.24 -val parallel_proofs = ref true;
    1.25 +val parallel_proofs = ref 1;
    1.26  
    1.27  fun future_enabled () =
    1.28 -  Future.enabled () andalso ! parallel_proofs andalso Future.is_worker ();
    1.29 +  Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
    1.30 +
    1.31 +fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
    1.32  
    1.33  
    1.34  (* future_result *)