670 val empty: T = Future.value []; |
670 val empty: T = Future.value []; |
671 fun init _ = empty; |
671 fun init _ = empty; |
672 ); |
672 ); |
673 |
673 |
674 fun proof_result immediate (tr, proof_trs) st = |
674 fun proof_result immediate (tr, proof_trs) st = |
675 if immediate orelse null proof_trs |
675 let val st' = command tr st in |
676 then fold_map command_result (tr :: proof_trs) st |>> Future.value |
676 if immediate orelse null proof_trs orelse not (can proof_of st') |
677 else |
677 then |
678 let |
678 let val (results, st'') = fold_map command_result proof_trs st' |
679 val st' = command tr st; |
679 in (Future.value ((tr, st') :: results), st'') end |
680 val (body_trs, end_tr) = split_last proof_trs; |
680 else |
681 val finish = Context.Theory o Proof_Context.theory_of; |
681 let |
682 |
682 val (body_trs, end_tr) = split_last proof_trs; |
683 val future_proof = Proof.global_future_proof |
683 val finish = Context.Theory o Proof_Context.theory_of; |
684 (fn prf => |
684 |
685 Goal.fork_name "Toplevel.future_proof" |
685 val future_proof = Proof.global_future_proof |
686 (fn () => |
686 (fn prf => |
687 let val (result, result_state) = |
687 Goal.fork_name "Toplevel.future_proof" |
688 (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) |
688 (fn () => |
689 => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) |
689 let val (result, result_state) = |
690 |> fold_map command_result body_trs ||> command end_tr; |
690 (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) |
691 in (result, presentation_context_of result_state) end)) |
691 => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) |
692 #-> Result.put; |
692 |> fold_map command_result body_trs ||> command end_tr; |
693 |
693 in (result, presentation_context_of result_state) end)) |
694 val st'' = st' |
694 #-> Result.put; |
695 |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof)); |
695 |
696 val result = |
696 val st'' = st' |
697 Result.get (presentation_context_of st'') |
697 |> command (tr |> set_print false |> reset_trans |> end_proof (K future_proof)); |
698 |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]); |
698 val result = |
699 |
699 Result.get (presentation_context_of st'') |
700 in (result, st'') end; |
700 |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]); |
|
701 |
|
702 in (result, st'') end |
|
703 end; |
701 |
704 |
702 end; |
705 end; |