# HG changeset patch
# User wenzelm
# Date 1231694315 -3600
# Node ID 34b9652b2f45999c65d2d446dcf3e999a4ee80fb
# Parent  a5d0c3cf305fe762856c848cfcce0c0ae10dfeeb
added Goal.future_enabled abstraction -- now also checks that this is already
  a future task, which excludes interactive commands of the old toplevel;

diff -r a5d0c3cf305f -r 34b9652b2f45 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jan 11 17:34:02 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Jan 11 18:18:35 2009 +0100
@@ -1041,7 +1041,7 @@
 local
 
 fun future_terminal_proof proof1 proof2 meths int state =
-  if int orelse is_relevant state orelse not (Future.enabled () andalso ! Goal.parallel_proofs)
+  if int orelse is_relevant state orelse not (Goal.future_enabled ())
   then proof1 meths state
   else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
 
diff -r a5d0c3cf305f -r 34b9652b2f45 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Sun Jan 11 17:34:02 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Sun Jan 11 18:18:35 2009 +0100
@@ -34,8 +34,7 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove ctxt xs asms prop tac =
-  (if Future.enabled () andalso ! Goal.parallel_proofs then Goal.prove_future else Goal.prove)
-    ctxt xs asms prop
+  (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     (fn args => fn st =>
       if ! quick_and_dirty
       then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
diff -r a5d0c3cf305f -r 34b9652b2f45 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jan 11 17:34:02 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Jan 11 18:18:35 2009 +0100
@@ -745,7 +745,7 @@
   let
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
-    val immediate = not (Future.enabled () andalso ! Goal.parallel_proofs);
+    val immediate = not (Goal.future_enabled ());
     val (results, end_state) = fold_map (proof_result immediate) input toplevel;
     val _ =
       (case end_state of
diff -r a5d0c3cf305f -r 34b9652b2f45 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Jan 11 17:34:02 2009 +0100
+++ b/src/Pure/goal.ML	Sun Jan 11 18:18:35 2009 +0100
@@ -20,6 +20,7 @@
   val conclude: thm -> thm
   val finish: thm -> thm
   val norm_result: thm -> thm
+  val future_enabled: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -92,6 +93,14 @@
   #> Drule.zero_var_indexes;
 
 
+(* future_enabled *)
+
+val parallel_proofs = ref true;
+
+fun future_enabled () =
+  Future.enabled () andalso ! parallel_proofs andalso is_some (Future.thread_data ());
+
+
 (* future_result *)
 
 fun future_result ctxt result prop =
@@ -124,8 +133,6 @@
       |> fold (Thm.elim_implies o Thm.assume) assms;
   in local_result end;
 
-val parallel_proofs = ref true;
-
 
 
 (** tactical theorem proving **)
@@ -175,8 +182,7 @@
             else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
           end);
     val res =
-      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse
-        not (Future.enabled () andalso ! parallel_proofs)
+      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
       then result ()
       else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
   in