Show diffs in "Show Proof."

Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output

9 files changed, 125 insertions, 5 deletions

diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst
new file mode 100644
index 0000000000..c1df728c5c
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst
@@ -0,0 +1,6 @@
+- Optionally highlight the differences between successive proof steps in the
+  :cmd:`Show Proof` command.  Experimental; only available in coqtop
+  and Proof General for now, may be supported in other IDEs
+  in the future.
+  (`#10494 <https://github.com/coq/coq/pull/10494>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 57a54bc0ad..00f8269dc3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -535,7 +535,7 @@ Requesting information
             eexists ?[n].
             Show n.
 
-   .. cmdv:: Show Proof
+   .. cmdv:: Show Proof {? Diffs {? removed } }
       :name: Show Proof
 
       Displays the proof term generated by the tactics
@@ -544,6 +544,12 @@ Requesting information
       constructed. Each hole is an existential variable, which appears as a
       question mark followed by an identifier.
 
+      Experimental: Specifying “Diffs” highlights the difference between the
+      current and previous proof step.  By default, the command shows the
+      output once with additions highlighted.  Including “removed” shows
+      the output twice: once showing removals and once showing additions.
+      It does not examine the :opt:`Diffs` option.  See :ref:`showing_diffs`.
+
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
 
@@ -624,8 +630,11 @@ Showing differences between proof steps
 ---------------------------------------
 
 
-Coq can automatically highlight the differences between successive proof steps and between
-values in some error messages.
+Coq can automatically highlight the differences between successive proof steps
+and between values in some error messages.  Also, as an experimental feature,
+Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof`
+command, but only, for now, when using coqtop and Proof General.
+
 For example, the following screenshots of CoqIDE and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index f6fca91eea..a806ab7123 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -16,6 +16,9 @@ val write_diffs_option : string -> unit
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
 
+(** Returns true if the diffs option is "removed" *)
+val show_removed : unit -> bool
+
 (** controls whether color output is enabled *)
 val write_color_enabled : bool -> unit
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 413c6540a3..47bb0a6af0 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -55,8 +55,7 @@ let get_current_goal_context pf =
     let env = Global.env () in
     Evd.from_env env, env
 
-let get_current_context pf =
-  let p = Proof_global.get_proof pf in
+let get_proof_context p =
   try get_goal_context_gen p 1
   with
   | NoSuchGoal ->
@@ -64,6 +63,10 @@ let get_current_context pf =
     let { Proof.sigma } = Proof.data p in
     sigma, Global.env ()
 
+let get_current_context pf =
+  let p = Proof_global.get_proof pf in
+  get_proof_context p
+
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
       | None -> tac
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index 30514191fa..11ce50b659 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env
 (** [get_current_goal_context ()] works as [get_goal_context 1] *)
 val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
 
+(** [get_proof_context ()] gets the goal context for the first subgoal
+    of the proof *)
+val get_proof_context : Proof.t -> Evd.evar_map * env
+
 (** [get_current_context ()] returns the context of the
   current focused goal. If there is no focused goal but there
   is a proof in progress, it returns the corresponding evar_map.
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out
new file mode 100644
index 0000000000..285a3bcd89
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.out
@@ -0,0 +1,42 @@
+

+Coq < Coq < 1 subgoal

+  

+  ============================

+  forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

+

+x < 

+x < 1 focused subgoal

+(shelved: 1)

+  i : nat

+  ============================

+  exists k : nat, i = ?j /\ ?j = k /\ i = k

+

+(fun i : nat =>

+ ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) ?j ?Goal)

+

+x < 1 focused subgoal

+(shelved: 2)

+  i : nat

+  ============================

+  i = ?j /\ ?j = ?k /\ i = ?k

+

+(fun i : nat =>

+ ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 

+   ?j (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) ?k ?Goal))

+

+x < 2 focused subgoals

+(shelved: 2)

+  i : nat

+  ============================

+  i = ?j

+

+subgoal 2 is:

+ ?j = ?k /\ i = ?k

+

+(fun i : nat =>

+ ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 

+   ?j

+   (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) 

+      ?k (conj ?Goal ?Goal0)))

+

+x < 

diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v
new file mode 100644
index 0000000000..4251c52cb4
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.v
@@ -0,0 +1,6 @@
+(* coq-prog-args: ("-color" "on" "-diffs" "on") *)
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.  Show Proof Diffs.
+  eexists.  Show Proof Diffs.
+  split.  Show Proof Diffs.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 1f319d2bfd..97f0e57d2e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -418,6 +418,50 @@ let rec vernac_loop ~state =
       Feedback.msg_notice (v 0 (goal ++ evars));
       vernac_loop ~state
 
+    | Some VernacShowProofDiffs removed ->
+      (* extension of Vernacentries.show_proof *)
+      let to_pp pstate =
+        let p = Option.get pstate in
+        let sigma, env = Pfedit.get_proof_context p in
+        let pprf = Proof.partial_proof p in
+        Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
+        (* We print nothing if there are no goals left *)
+      in
+
+      if not (Proof_diffs.color_enabled ()) then
+        CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
+      else begin
+        let out =
+          try
+            let n_pp = to_pp state.proof in
+            if true (*Proof_diffs.show_diffs ()*) then
+              let doc = state.doc in
+              let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
+              try
+                let o_pp = to_pp oproof in
+                let tokenize_string = Proof_diffs.tokenize_string in
+                let show_removed = Some removed in
+                Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
+              with
+              | Pfedit.NoSuchGoal
+              | Option.IsNone -> n_pp
+              | Pp_diff.Diff_Failure msg -> begin
+                (* todo: print the unparsable string (if we know it) *)
+                Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut()
+                    ++ str "Showing results without diff highlighting" );
+                n_pp
+                end
+            else
+              n_pp
+          with
+          | Pfedit.NoSuchGoal
+          | Option.IsNone ->
+            CErrors.user_err (str "No goals to show.")
+        in
+        Feedback.msg_notice out;
+      end;
+      vernac_loop ~state
+
     | None ->
       top_stderr (fnl ()); exit 0
 
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index e180d9e750..56fda58a25 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -22,6 +22,7 @@ type vernac_toplevel =
   | VernacQuit
   | VernacControl of vernac_control
   | VernacShowGoal of { gid : int; sid: int }
+  | VernacShowProofDiffs of bool
 
 module Toplevel_ : sig
   val vernac_toplevel : vernac_toplevel option Entry.t
@@ -59,6 +60,8 @@ GRAMMAR EXTEND Gram
       (* show a goal for the specified proof state *)
       | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." ->
           { Some (VernacShowGoal {gid; sid}) }
+      | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." ->
+        { Some (VernacShowProofDiffs (removed <> None)) }
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None