recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
authorwenzelm
Wed Aug 01 15:33:08 2012 +0200 (2012-08-01 ago)
changeset 486337cd32f9d4293
parent 48632 c028cf680a3e
child 48634 30a6e841390a
recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 01 15:32:36 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 01 15:33:08 2012 +0200
     1.3 @@ -672,31 +672,34 @@
     1.4  );
     1.5  
     1.6  fun proof_result immediate (tr, proof_trs) st =
     1.7 -  if immediate orelse null proof_trs
     1.8 -  then fold_map command_result (tr :: proof_trs) st |>> Future.value
     1.9 -  else
    1.10 -    let
    1.11 -      val st' = command tr st;
    1.12 -      val (body_trs, end_tr) = split_last proof_trs;
    1.13 -      val finish = Context.Theory o Proof_Context.theory_of;
    1.14 +  let val st' = command tr st in
    1.15 +    if immediate orelse null proof_trs orelse not (can proof_of st')
    1.16 +    then
    1.17 +      let val (results, st'') = fold_map command_result proof_trs st'
    1.18 +      in (Future.value ((tr, st') :: results), st'') end
    1.19 +    else
    1.20 +      let
    1.21 +        val (body_trs, end_tr) = split_last proof_trs;
    1.22 +        val finish = Context.Theory o Proof_Context.theory_of;
    1.23  
    1.24 -      val future_proof = Proof.global_future_proof
    1.25 -        (fn prf =>
    1.26 -          Goal.fork_name "Toplevel.future_proof"
    1.27 -            (fn () =>
    1.28 -              let val (result, result_state) =
    1.29 -                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.30 -                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.31 -                |> fold_map command_result body_trs ||> command end_tr;
    1.32 -              in (result, presentation_context_of result_state) end))
    1.33 -        #-> Result.put;
    1.34 +        val future_proof = Proof.global_future_proof
    1.35 +          (fn prf =>
    1.36 +            Goal.fork_name "Toplevel.future_proof"
    1.37 +              (fn () =>
    1.38 +                let val (result, result_state) =
    1.39 +                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.40 +                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.41 +                  |> fold_map command_result body_trs ||> command end_tr;
    1.42 +                in (result, presentation_context_of result_state) end))
    1.43 +          #-> Result.put;
    1.44  
    1.45 -      val st'' = st'
    1.46 -        |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.47 -      val result =
    1.48 -        Result.get (presentation_context_of st'')
    1.49 -        |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
    1.50 +        val st'' = st'
    1.51 +          |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof));
    1.52 +        val result =
    1.53 +          Result.get (presentation_context_of st'')
    1.54 +          |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
    1.55  
    1.56 -    in (result, st'') end;
    1.57 +      in (result, st'') end
    1.58 +  end;
    1.59  
    1.60  end;