761 |
761 |
762 fun atom_result tr st = |
762 fun atom_result tr st = |
763 let |
763 let |
764 val st' = |
764 val st' = |
765 if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then |
765 if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then |
766 setmp_thread_position tr (fn () => |
766 (Goal.fork_params |
767 (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr))) |
767 {name = "Toplevel.diag", pos = pos_of tr, |
768 (fn () => command tr st); st)) () |
768 pri = priority (timing_estimate true (Thy_Syntax.atom tr))} |
|
769 (fn () => command tr st); st) |
769 else command tr st; |
770 else command tr st; |
770 in (Result (tr, st'), st') end; |
771 in (Result (tr, st'), st') end; |
771 |
772 |
772 in |
773 in |
773 |
774 |
786 in (Result_List (head_result :: proof_results), st'') end |
787 in (Result_List (head_result :: proof_results), st'') end |
787 else |
788 else |
788 let |
789 let |
789 val finish = Context.Theory o Proof_Context.theory_of; |
790 val finish = Context.Theory o Proof_Context.theory_of; |
790 |
791 |
791 val future_proof = Proof.future_proof |
792 val future_proof = |
792 (fn state => |
793 Proof.future_proof (fn state => |
793 setmp_thread_position head_tr (fn () => |
794 Goal.fork_params |
794 Goal.fork_name "Toplevel.future_proof" |
795 {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate} |
795 (priority estimate) |
796 (fn () => |
796 (fn () => |
797 let |
797 let |
798 val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st'; |
798 val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st'; |
799 val prf' = Proof_Node.apply (K state) prf; |
799 val prf' = Proof_Node.apply (K state) prf; |
800 val (result, result_state) = |
800 val (result, result_state) = |
801 State (SOME (Proof (prf', (finish, orig_gthy))), prev) |
801 State (SOME (Proof (prf', (finish, orig_gthy))), prev) |
802 |> fold_map element_result body_elems ||> command end_tr; |
802 |> fold_map element_result body_elems ||> command end_tr; |
803 in (Result_List result, presentation_context_of result_state) end)) |
803 in (Result_List result, presentation_context_of result_state) end)) ()) |
|
804 #> (fn (res, state') => state' |> put_result (Result_Future res)); |
804 #> (fn (res, state') => state' |> put_result (Result_Future res)); |
805 |
805 |
806 val forked_proof = |
806 val forked_proof = |
807 proof (future_proof #> |
807 proof (future_proof #> |
808 (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o |
808 (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o |