future proofs: more robust check via Future.enabled;
authorwenzelm
Fri Dec 12 12:14:02 2008 +0100 (2008-12-12)
changeset 2908895a239a5e055
parent 29087 40fbcea084ff
child 29089 8cffa980bd93
child 29090 bbfac5fd8d78
child 29097 68245155eb58
child 29129 9925cf74b23b
child 29212 242b0bc2172c
future proofs: more robust check via Future.enabled;
src/Pure/Isar/skip_proof.ML
src/Pure/Thy/thy_info.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Dec 11 22:53:50 2008 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Fri Dec 12 12:14:02 2008 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
     1.5  
     1.6  fun prove ctxt xs asms prop tac =
     1.7 -  (if ! future_scheduler then Goal.prove_future else Goal.prove) ctxt xs asms prop
     1.8 +  (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     1.9      (fn args => fn st =>
    1.10        if ! quick_and_dirty
    1.11        then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
     2.1 --- a/src/Pure/Thy/thy_info.ML	Thu Dec 11 22:53:50 2008 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Dec 12 12:14:02 2008 +0100
     2.3 @@ -375,7 +375,7 @@
     2.4      else if Multithreading.self_critical () then
     2.5       (warning (loader_msg "no multithreading within critical section" []);
     2.6        schedule_seq tasks)
     2.7 -    else if ! future_scheduler then future_schedule tasks
     2.8 +    else if Future.enabled () then future_schedule tasks
     2.9      else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
    2.10    end;
    2.11  
     3.1 --- a/src/Pure/goal.ML	Thu Dec 11 22:53:50 2008 +0100
     3.2 +++ b/src/Pure/goal.ML	Fri Dec 12 12:14:02 2008 +0100
     3.3 @@ -177,7 +177,8 @@
     3.4              else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
     3.5            end);
     3.6      val res =
     3.7 -      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
     3.8 +      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
     3.9 +      then result ()
    3.10        else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
    3.11    in
    3.12      Conjunction.elim_balanced (length props) res