1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 20:55:48 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 26 11:57:19 2013 +0100
     1.3 @@ -95,6 +95,7 @@
     1.4    val put_timing: Time.time -> transition -> transition
     1.5    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.6    val command: transition -> state -> state
     1.7 +  val atom_result: transition -> state -> (transition * state) * state
     1.8    val element_result: transition Thy_Syntax.element -> state ->
     1.9      (transition * state) list future * state
    1.10  end;
    1.11 @@ -704,22 +705,26 @@
    1.12    fun init _ = empty;
    1.13  );
    1.14  
    1.15 +fun priority trs =
    1.16 +  let val estimate = fold (curry Time.+ o get_timing) trs Time.zeroTime in
    1.17 +    if estimate = Time.zeroTime then ~1
    1.18 +    else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
    1.19 +  end;
    1.20 +
    1.21 +fun atom_result tr st =
    1.22 +  let val st' = command tr st
    1.23 +  in ((tr, st'), st') end;
    1.24 +
    1.25  fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
    1.26    let
    1.27 -    val future_enabled = Goal.future_enabled ();
    1.28 -
    1.29 -    fun atom_result tr st =
    1.30 -      let val st' = command tr st
    1.31 -      in ((tr, st'), st') end;
    1.32 -
    1.33      val proof_trs =
    1.34        (case opt_proof of
    1.35          NONE => []
    1.36        | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
    1.37  
    1.38 -    val st' = command head_tr st;
    1.39 +    val (_, st') = atom_result head_tr st;
    1.40    in
    1.41 -    if not future_enabled orelse is_ignored head_tr orelse
    1.42 +    if not (Goal.future_enabled ()) orelse is_ignored head_tr orelse
    1.43        null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    1.44      then
    1.45        let val (results, st'') = fold_map atom_result proof_trs st'
    1.46 @@ -729,14 +734,9 @@
    1.47          val (body_trs, end_tr) = split_last proof_trs;
    1.48          val finish = Context.Theory o Proof_Context.theory_of;
    1.49  
    1.50 -        val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
    1.51 -        val pri =
    1.52 -          if estimate = Time.zeroTime then ~1
    1.53 -          else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.54 -
    1.55          val future_proof = Proof.global_future_proof
    1.56            (fn prf =>
    1.57 -            Goal.fork_name "Toplevel.future_proof" pri
    1.58 +            Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    1.59                (fn () =>
    1.60                  let val (result, result_state) =
    1.61                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)