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

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

2 files changed, 28 insertions, 0 deletions

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 43f70dfecc..dd372ecb0f 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -252,6 +252,9 @@ let pp_of_type env sigma ty =
 let pr_leconstr_env ?lax ?inctx ?scope env sigma t =
   Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t)
 
+let pr_econstr_env ?lax ?inctx ?scope env sigma t =
+  Ppconstr.pr_constr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t)
+
 let pr_lconstr_env ?lax ?inctx ?scope env sigma c =
   pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c)
 
@@ -660,3 +663,22 @@ let make_goal_map op np =
   let ng_to_og = make_goal_map_i op np in
   (*db_goal_map op np ng_to_og;*)
   ng_to_og
+
+let diff_proofs ~diff_opt ?old proof =
+  let pp_proof p =
+    let sigma, env = Proof.get_proof_context p in
+    let pprf = Proof.partial_proof p in
+    Pp.prlist_with_sep Pp.fnl (pr_econstr_env env sigma) pprf in
+  match diff_opt with
+  | DiffOff -> pp_proof proof
+  | _ -> begin
+      try
+        let n_pp = pp_proof proof in
+        let o_pp = match old with
+          | None -> Pp.mt()
+          | Some old -> pp_proof old in
+        let show_removed = Some (diff_opt = DiffRemoved) in
+        Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
+      with
+      | Pp_diff.Diff_Failure msg -> Pp.str msg
+    end
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index ea64439456..6bdd7004fb 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -25,6 +25,10 @@ val write_color_enabled : bool -> unit
 (** true indicates that color output is enabled *)
 val color_enabled : unit -> bool
 
+type diffOpt = DiffOff | DiffOn | DiffRemoved
+
+val string_to_diffs : string -> diffOpt
+
 open Evd
 open Environ
 open Constr
@@ -84,3 +88,5 @@ type hyp_info = {
 }
 
 val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list
+
+val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t