added Goal.future_enabled abstraction -- now also checks that this is already
authorwenzelm
Sun Jan 11 18:18:35 2009 +0100 (2009-01-11)
changeset 2944834b9652b2f45
parent 29447 a5d0c3cf305f
child 29449 6e7745d35a30
child 29451 5f0cb3fa530d
added Goal.future_enabled abstraction -- now also checks that this is already
a future task, which excludes interactive commands of the old toplevel;
src/Pure/Isar/proof.ML
src/Pure/Isar/skip_proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Jan 11 17:34:02 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Jan 11 18:18:35 2009 +0100
     1.3 @@ -1041,7 +1041,7 @@
     1.4  local
     1.5  
     1.6  fun future_terminal_proof proof1 proof2 meths int state =
     1.7 -  if int orelse is_relevant state orelse not (Future.enabled () andalso ! Goal.parallel_proofs)
     1.8 +  if int orelse is_relevant state orelse not (Goal.future_enabled ())
     1.9    then proof1 meths state
    1.10    else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
    1.11  
     2.1 --- a/src/Pure/Isar/skip_proof.ML	Sun Jan 11 17:34:02 2009 +0100
     2.2 +++ b/src/Pure/Isar/skip_proof.ML	Sun Jan 11 18:18:35 2009 +0100
     2.3 @@ -34,8 +34,7 @@
     2.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
     2.5  
     2.6  fun prove ctxt xs asms prop tac =
     2.7 -  (if Future.enabled () andalso ! Goal.parallel_proofs then Goal.prove_future else Goal.prove)
     2.8 -    ctxt xs asms prop
     2.9 +  (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
    2.10      (fn args => fn st =>
    2.11        if ! quick_and_dirty
    2.12        then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
     3.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jan 11 17:34:02 2009 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Jan 11 18:18:35 2009 +0100
     3.3 @@ -745,7 +745,7 @@
     3.4    let
     3.5      val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
     3.6  
     3.7 -    val immediate = not (Future.enabled () andalso ! Goal.parallel_proofs);
     3.8 +    val immediate = not (Goal.future_enabled ());
     3.9      val (results, end_state) = fold_map (proof_result immediate) input toplevel;
    3.10      val _ =
    3.11        (case end_state of
     4.1 --- a/src/Pure/goal.ML	Sun Jan 11 17:34:02 2009 +0100
     4.2 +++ b/src/Pure/goal.ML	Sun Jan 11 18:18:35 2009 +0100
     4.3 @@ -20,6 +20,7 @@
     4.4    val conclude: thm -> thm
     4.5    val finish: thm -> thm
     4.6    val norm_result: thm -> thm
     4.7 +  val future_enabled: unit -> bool
     4.8    val future_result: Proof.context -> thm future -> term -> thm
     4.9    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    4.10    val prove_multi: Proof.context -> string list -> term list -> term list ->
    4.11 @@ -92,6 +93,14 @@
    4.12    #> Drule.zero_var_indexes;
    4.13  
    4.14  
    4.15 +(* future_enabled *)
    4.16 +
    4.17 +val parallel_proofs = ref true;
    4.18 +
    4.19 +fun future_enabled () =
    4.20 +  Future.enabled () andalso ! parallel_proofs andalso is_some (Future.thread_data ());
    4.21 +
    4.22 +
    4.23  (* future_result *)
    4.24  
    4.25  fun future_result ctxt result prop =
    4.26 @@ -124,8 +133,6 @@
    4.27        |> fold (Thm.elim_implies o Thm.assume) assms;
    4.28    in local_result end;
    4.29  
    4.30 -val parallel_proofs = ref true;
    4.31 -
    4.32  
    4.33  
    4.34  (** tactical theorem proving **)
    4.35 @@ -175,8 +182,7 @@
    4.36              else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
    4.37            end);
    4.38      val res =
    4.39 -      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse
    4.40 -        not (Future.enabled () andalso ! parallel_proofs)
    4.41 +      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
    4.42        then result ()
    4.43        else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
    4.44    in