removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
authorwenzelm
Fri Aug 06 14:35:04 2010 +0200 (2010-08-06)
changeset 382181408f753bd75
parent 38217 c75e9dc841c7
child 38219 521f10c13e61
removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
src/Pure/Isar/proof.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Aug 06 12:38:02 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Aug 06 14:35:04 2010 +0200
     1.3 @@ -1074,8 +1074,7 @@
     1.4  local
     1.5  
     1.6  fun future_terminal_proof proof1 proof2 meths int state =
     1.7 -  if not (Goal.local_future_enforced ()) andalso
     1.8 -    int orelse is_relevant state orelse not (Goal.local_future_enabled ())
     1.9 +  if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
    1.10    then proof1 meths state
    1.11    else snd (proof2 (fn state' => Goal.fork (fn () => ((), proof1 meths state'))) state);
    1.12  
     2.1 --- a/src/Pure/goal.ML	Fri Aug 06 12:38:02 2010 +0200
     2.2 +++ b/src/Pure/goal.ML	Fri Aug 06 14:35:04 2010 +0200
     2.3 @@ -26,7 +26,6 @@
     2.4    val fork: (unit -> 'a) -> 'a future
     2.5    val future_enabled: unit -> bool
     2.6    val local_future_enabled: unit -> bool
     2.7 -  val local_future_enforced: unit -> bool
     2.8    val future_result: Proof.context -> thm future -> term -> thm
     2.9    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    2.10    val prove_multi: Proof.context -> string list -> term list -> term list ->
    2.11 @@ -112,7 +111,6 @@
    2.12    Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
    2.13  
    2.14  fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
    2.15 -fun local_future_enforced () = future_enabled () andalso ! parallel_proofs >= 3;
    2.16  
    2.17  
    2.18  (* future_result *)