712 type T = (transition * state) list future; |
712 type T = (transition * state) list future; |
713 val empty: T = Future.value []; |
713 val empty: T = Future.value []; |
714 fun init _ = empty; |
714 fun init _ = empty; |
715 ); |
715 ); |
716 |
716 |
|
717 fun done_proof state = |
|
718 if can (Proof.assert_bottom true) state |
|
719 then Proof.global_done_proof state |
|
720 else Proof.context_of (Proof.local_done_proof state); |
|
721 |
|
722 fun proof_future_enabled st = |
|
723 (case try proof_of st of |
|
724 NONE => false |
|
725 | SOME state => |
|
726 not (Proof.is_relevant state) andalso |
|
727 (if can (Proof.assert_bottom true) state |
|
728 then Goal.future_enabled () |
|
729 else Goal.future_enabled_nested 2)); |
|
730 |
717 fun priority elem = |
731 fun priority elem = |
718 let |
732 let |
719 val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime; |
733 val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime; |
720 in |
734 in |
721 if estimate = Time.zeroTime then ~1 |
735 if estimate = Time.zeroTime then ~1 |
732 else command tr st; |
746 else command tr st; |
733 in ((tr, st'), st') end; |
747 in ((tr, st'), st') end; |
734 |
748 |
735 in |
749 in |
736 |
750 |
737 fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st = |
751 fun element_result (Thy_Syntax.Element (tr, NONE)) st = |
738 let |
752 let val (result, st') = atom_result tr st |
739 val proof_trs = |
753 in (Future.value [result], st') end |
740 (case opt_proof of |
754 | element_result (Thy_Syntax.Element (head_tr, SOME proof)) st = |
741 NONE => [] |
|
742 | SOME (a, b) => maps Thy_Syntax.flat_element a @ [b]); |
|
743 |
|
744 val (_, st') = atom_result head_tr st; |
|
745 in |
|
746 if not (Goal.future_enabled ()) orelse null proof_trs orelse |
|
747 not (can proof_of st') orelse Proof.is_relevant (proof_of st') |
|
748 then |
|
749 let val (results, st'') = fold_map atom_result proof_trs st' |
|
750 in (Future.value ((head_tr, st') :: results), st'') end |
|
751 else |
|
752 let |
755 let |
753 val (body_trs, end_tr) = split_last proof_trs; |
756 val (head_result, st') = atom_result head_tr st; |
754 val finish = Context.Theory o Proof_Context.theory_of; |
757 val (body_elems, end_tr) = proof; |
755 |
758 val body_trs = maps Thy_Syntax.flat_element body_elems; |
756 val future_proof = Proof.future_proof |
759 in |
757 (fn prf => |
760 if not (proof_future_enabled st') |
758 setmp_thread_position head_tr (fn () => |
761 then |
759 Goal.fork_name "Toplevel.future_proof" |
762 let val (proof_results, st'') = fold_map atom_result (body_trs @ [end_tr]) st' |
760 (priority (Thy_Syntax.Element (empty, opt_proof))) |
763 in (Future.value (head_result :: proof_results), st'') end |
761 (fn () => |
764 else |
762 let val (result, result_state) = |
765 let |
763 (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) |
766 val finish = Context.Theory o Proof_Context.theory_of; |
764 => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) |
767 |
765 |> fold_map atom_result body_trs ||> command end_tr; |
768 val future_proof = Proof.future_proof |
766 in (result, presentation_context_of result_state) end)) ()) |
769 (fn prf => |
767 #> (fn (result, state') => state' |> Proof.global_done_proof |> Result.put result); |
770 setmp_thread_position head_tr (fn () => |
768 |
771 Goal.fork_name "Toplevel.future_proof" |
769 val st'' = st' |
772 (priority (Thy_Syntax.Element (empty, SOME proof))) |
770 |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof)); |
773 (fn () => |
771 val result = |
774 let val (result, result_state) = |
772 Result.get (presentation_context_of st'') |
775 (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) |
773 |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]); |
776 => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) |
774 |
777 |> fold_map atom_result body_trs ||> command end_tr; |
775 in (result, st'') end |
778 in (result, presentation_context_of result_state) end)) ()) |
776 end; |
779 #> (fn (result, state') => state' |> done_proof |> Result.put result); |
777 |
780 |
778 end; |
781 val st'' = st' |
779 |
782 |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof)); |
780 end; |
783 val result = |
|
784 Result.get (presentation_context_of st'') |
|
785 |> Future.map (fn body_results => head_result :: body_results @ [(end_tr, st'')]); |
|
786 |
|
787 in (result, st'') end |
|
788 end; |
|
789 |
|
790 end; |
|
791 |
|
792 end; |