src/Pure/goal.ML
changeset 37186 349e9223c685
parent 36613 f3157c288aca
child 37690 b16231572c61
     1.1 --- a/src/Pure/goal.ML	Sat May 29 17:26:02 2010 +0200
     1.2 +++ b/src/Pure/goal.ML	Sat May 29 19:46:29 2010 +0200
     1.3 @@ -23,8 +23,10 @@
     1.4    val check_finished: Proof.context -> thm -> unit
     1.5    val finish: Proof.context -> thm -> thm
     1.6    val norm_result: thm -> thm
     1.7 +  val fork: (unit -> 'a) -> 'a future
     1.8    val future_enabled: unit -> bool
     1.9    val local_future_enabled: unit -> bool
    1.10 +  val local_future_enforced: unit -> bool
    1.11    val future_result: Proof.context -> thm future -> term -> thm
    1.12    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    1.13    val prove_multi: Proof.context -> string list -> term list -> term list ->
    1.14 @@ -100,7 +102,14 @@
    1.15    #> Drule.zero_var_indexes;
    1.16  
    1.17  
    1.18 -(* future_enabled *)
    1.19 +(* parallel proofs *)
    1.20 +
    1.21 +fun fork e = Future.fork_pri ~1 (fn () =>
    1.22 +  let
    1.23 +    val _ = Output.status (Markup.markup Markup.forked "");
    1.24 +    val x = e ();  (*sic*)
    1.25 +    val _ = Output.status (Markup.markup Markup.joined "");
    1.26 +  in x end);
    1.27  
    1.28  val parallel_proofs = Unsynchronized.ref 1;
    1.29  
    1.30 @@ -108,6 +117,7 @@
    1.31    Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
    1.32  
    1.33  fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
    1.34 +fun local_future_enforced () = future_enabled () andalso ! parallel_proofs >= 3;
    1.35  
    1.36  
    1.37  (* future_result *)
    1.38 @@ -198,7 +208,7 @@
    1.39      val res =
    1.40        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
    1.41        then result ()
    1.42 -      else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
    1.43 +      else future_result ctxt' (fork result) (Thm.term_of stmt);
    1.44    in
    1.45      Conjunction.elim_balanced (length props) res
    1.46      |> map (Assumption.export false ctxt' ctxt)