Merge PR #8182: Handle diffs better for the "Undo" command.

4 files changed, 30 insertions, 10 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
diff --git a/stm/stm.ml b/stm/stm.ml
index e15b6048ba..2e9bf71e49 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1103,7 +1103,8 @@ module Backtrack : sig
   val branches_of : Stateid.t -> backup
 
   (* Returns the state that the command should backtract to *)
-  val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when
+  val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when
+  val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
 
 end = struct (* {{{ *)
 
@@ -1161,7 +1162,17 @@ end = struct (* {{{ *)
              " If your use is intentional, you may want to disable this warning and pass" ^
              " the \"-async-proofs-cache force\" option to Coq."))
 
-  let undo_vernac_classifier v =
+  let back_tactic n (id,_,_,tactic,undo) =
+    let value = (if tactic then 1 else 0) - undo in
+    if Int.equal n 0 then `Stop id else `Cont (n-value)
+
+  let get_proof ~doc id =
+    let open Vernacstate in
+    match state_of_id ~doc id with
+    | `Valid (Some vstate) -> Some (Proof_global.proof_of_state vstate.proof)
+    | _ -> None
+
+  let undo_vernac_classifier v ~doc =
     if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force
     then undo_costly_in_batch_mode v;
     try
@@ -1185,9 +1196,7 @@ end = struct (* {{{ *)
           oid, VtNow
       | VernacUndo n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_,tactic,undo) ->
-            let value = (if tactic then 1 else 0) - undo in
-            if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
+          let oid = fold_until back_tactic n id in
           oid, VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
@@ -1220,8 +1229,16 @@ end = struct (* {{{ *)
        CErrors.user_err ~hdr:"undo_vernac_classifier"
         Pp.(str "Cannot undo")
 
+  let get_prev_proof ~doc id =
+    try
+      let did = fold_until back_tactic 1 id in
+      get_proof ~doc did
+    with Not_found -> None
+
 end (* }}} *)
 
+let get_prev_proof = Backtrack.get_prev_proof
+
 let hints = ref Aux_file.empty_aux_file
 let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
@@ -2785,7 +2802,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       match c with
       (* Meta *)
       | VtMeta, _ ->
-        let id, w = Backtrack.undo_vernac_classifier expr in
+        let id, w = Backtrack.undo_vernac_classifier expr ~doc in
         process_back_meta_command ~newtip ~head id x w
 
       (* Query *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 50e7f06095..7f70ea18da 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -110,6 +110,10 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
   bool -> Vernacexpr.vernac_control CAst.t ->
   doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
+(* Returns the proof state before the last tactic that was applied at or before
+the specified state.  Used to compute proof diffs. *)
+val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
+
 (* [query at ?report_with cmd] Executes [cmd] at a given state [at],
    throwing away side effects except messages. Feedback will
    be sent with [report_with], which defaults to the dummy state id *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 7b7e1b16c0..9e16b97608 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -376,7 +376,8 @@ let rec vernac_loop ~state =
       else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
     | {v=VernacControl c; loc} ->
       let nstate = Vernac.process_expr ~state (make ?loc c) in
-      top_goal_print state.proof nstate.proof;
+      let dproof = Stm.get_prev_proof ~doc:state.doc (Stm.get_current_state ~doc:state.doc) in
+      top_goal_print dproof nstate.proof;
       vernac_loop ~state:nstate
   with
   | Stm.End_of_input ->