diff options
| author | Enrico Tassi | 2018-08-01 11:21:49 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-08-01 11:21:49 +0200 |
| commit | a257ddce0ef35b8596e71377e9a1967baefebea4 (patch) | |
| tree | 0a7865ccdd9e18eceefa6e3773af51e152f4005f /ide | |
| parent | e8dbb311c82acb5cdf6d2f81dd6a1df503a7a123 (diff) | |
| parent | 7d2a9df50d519607c23a97c8973cb7d026d3d8d0 (diff) | |
Merge PR #8182: Handle diffs better for the "Undo" command.
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 |