Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol

Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego

4 files changed, 13 insertions, 38 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index eb386ea3e8..d587e57fd8 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -508,6 +508,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> set_query oval PrintConfig
     |"-debug" -> Coqinit.set_debug (); oval
+    |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval
     |"-diffs" ->
       add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ()))
     |"-stm-debug" -> Stm.stm_debug := true; oval
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 88924160ff..6460378edc 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -371,41 +371,13 @@ let exit_on_error =
   declare_bool_option_and_ref ~depr:false ~key:["Coqtop";"Exit";"On";"Error"]
     ~value:false
 
-(* XXX: This is duplicated with Vernacentries.show_proof , at some
-   point we should consolidate the code *)
-let show_proof_diff_to_pp pstate =
-  let p = Option.get pstate in
-  let sigma, env = Proof.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
-
-let show_proof_diff_cmd ~state removed =
+let show_proof_diff_cmd ~state diff_opt =
   let open Vernac.State in
-  try
-    let n_pp = show_proof_diff_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 = show_proof_diff_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
-      | Proof.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
-  | Proof.NoSuchGoal _
-  | Option.IsNone ->
-    CErrors.user_err (str "No goals to show.")
+  match state.proof with
+  | None -> CErrors.user_err (str "No proofs to diff.")
+  | Some proof ->
+      let old = Stm.get_prev_proof ~doc:state.doc state.sid in
+      Proof_diffs.diff_proofs ~diff_opt ?old proof
 
 let process_toplevel_command ~state stm =
   let open Vernac.State in
@@ -444,12 +416,12 @@ let process_toplevel_command ~state stm =
     Feedback.msg_notice (v 0 (goal ++ evars));
     state
 
-  | VernacShowProofDiffs removed ->
+  | VernacShowProofDiffs diff_opt ->
     (* We print nothing if there are no goals left *)
     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
-      let out = show_proof_diff_cmd ~state removed in
+      let out = show_proof_diff_cmd ~state diff_opt in
       Feedback.msg_notice out;
     state
 
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 1902103a3e..ef79f4562e 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -20,7 +20,7 @@ type vernac_toplevel =
   | VernacQuit
   | VernacControl of vernac_control
   | VernacShowGoal of { gid : int; sid: int }
-  | VernacShowProofDiffs of bool
+  | VernacShowProofDiffs of Proof_diffs.diffOpt
 
 module Toplevel_ : sig
   val vernac_toplevel : vernac_toplevel option Entry.t
@@ -52,7 +52,8 @@ GRAMMAR EXTEND Gram
       | 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)) }
+        { Some (VernacShowProofDiffs
+          (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) }
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 732ad05b26..6fb5f821ee 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -72,6 +72,7 @@ let print_usage_common co command =
 \n  -init-file f           set the rcfile to f\
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
+\n  -xml-debug             debug mode and print XML messages to/from coqide\
 \n  -diffs (on|off|removed) highlight differences between proof steps\
 \n  -stm-debug             STM debug mode (will trace every transaction)\
 \n  -noglob                do not dump globalizations\