src/Pure/Isar/toplevel.ML
changeset 47417 9679bab23f93
parent 47416 df8fc0567a3d
child 47425 45e570742e73
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Apr 10 21:31:05 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Apr 10 22:53:41 2012 +0200
     1.3 @@ -659,50 +659,43 @@
     1.4  
     1.5  fun command_result tr st =
     1.6    let val st' = command tr st
     1.7 -  in (st', st') end;
     1.8 +  in ((tr, st'), st') end;
     1.9  
    1.10  
    1.11  (* scheduled proof result *)
    1.12  
    1.13 -structure States = Proof_Data
    1.14 +structure Result = Proof_Data
    1.15  (
    1.16 -  type T = state list future option;
    1.17 -  fun init _ = NONE;
    1.18 +  type T = (transition * state) list future;
    1.19 +  val empty: T = Future.value [];
    1.20 +  fun init _ = empty;
    1.21  );
    1.22  
    1.23  fun proof_result immediate (tr, proof_trs) st =
    1.24 -  let val st' = command tr st in
    1.25 -    if immediate orelse null proof_trs orelse not (can proof_of st')
    1.26 -    then
    1.27 -      let val (states, st'') = fold_map command_result proof_trs st'
    1.28 -      in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end
    1.29 -    else
    1.30 -      let
    1.31 -        val (body_trs, end_tr) = split_last proof_trs;
    1.32 -        val finish = Context.Theory o Proof_Context.theory_of;
    1.33 +  if immediate orelse null proof_trs
    1.34 +  then fold_map command_result (tr :: proof_trs) st |>> Future.value
    1.35 +  else
    1.36 +    let
    1.37 +      val st' = command tr st;
    1.38 +      val (body_trs, end_tr) = split_last proof_trs;
    1.39 +      val finish = Context.Theory o Proof_Context.theory_of;
    1.40  
    1.41 -        val future_proof = Proof.global_future_proof
    1.42 -          (fn prf =>
    1.43 -            Goal.fork_name "Toplevel.future_proof"
    1.44 -              (fn () =>
    1.45 -                let val (states, result_state) =
    1.46 -                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.47 -                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.48 -                  |> fold_map command_result body_trs
    1.49 -                  ||> command (end_tr |> set_print false);
    1.50 -                in (states, presentation_context_of result_state) end))
    1.51 -          #> (fn (states, ctxt) => States.put (SOME states) ctxt);
    1.52 +      val future_proof = Proof.global_future_proof
    1.53 +        (fn prf =>
    1.54 +          Goal.fork_name "Toplevel.future_proof"
    1.55 +            (fn () =>
    1.56 +              let val (result, result_state) =
    1.57 +                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.58 +                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.59 +                |> fold_map command_result body_trs ||> command end_tr;
    1.60 +              in (result, presentation_context_of result_state) end))
    1.61 +        #-> Result.put;
    1.62  
    1.63 -        val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
    1.64 +      val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
    1.65 +      val result =
    1.66 +        Result.get (presentation_context_of st'')
    1.67 +        |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
    1.68  
    1.69 -        val states =
    1.70 -          (case States.get (presentation_context_of st'') of
    1.71 -            NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
    1.72 -          | SOME states => states);
    1.73 -        val result = states
    1.74 -          |> Future.map (fn sts => (tr, st') :: (body_trs ~~ sts) @ [(end_tr, st'')]);
    1.75 -
    1.76 -      in (result, st'') end
    1.77 -  end;
    1.78 +    in (result, st'') end;
    1.79  
    1.80  end;