diff options
| author | Jim Fehrle | 2018-07-07 21:17:32 -0400 |
|---|---|---|
| committer | Jim Fehrle | 2018-07-31 16:32:42 -0700 |
| commit | 7d2a9df50d519607c23a97c8973cb7d026d3d8d0 (patch) | |
| tree | b4194c9684b7e249fd712ecb4edfc135193a18a5 /ide | |
| parent | e130be4ccb68e0876ed789d295ae9a94d4358bf9 (diff) | |
Code to handle "Back" command for diffs.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index 854b1abe31..417ade51fd 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -211,15 +211,13 @@ let add_diffs oldp newp intf = { intf with fg_goals = { first_goal with goal_hyp = hyps_pp_list; goal_ccl = concl_pp } :: tl } let goals () = - let oldp = - try Some (Proof_global.give_me_the_proof ()) - with Proof_global.NoCurrentProof -> None in let doc = get_doc () in set_doc @@ Stm.finish ~doc; try let newp = Proof_global.give_me_the_proof () in let intf = export_pre_goals (Proof.map_structured_proof newp process_goal) in if Proof_diffs.show_diffs () then + let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in try Some (add_diffs oldp (Some newp) intf) with Pp_diff.Diff_Failure _ -> Some intf |