Add an XML message for "Show Proof Diffs"

Add menu item that uses this

1 files changed, 22 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