added Goal.future_enabled abstraction -- now also checks that this is already
a future task, which excludes interactive commands of the old toplevel;
--- 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'))));
--- 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
--- 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
--- 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