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

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

25 files changed, 231 insertions, 80 deletions

diff --git a/doc/changelog/09-coqide/12874-show_proof_diffs.rst b/doc/changelog/09-coqide/12874-show_proof_diffs.rst
new file mode 100644
index 0000000000..51bebad9be
--- /dev/null
+++ b/doc/changelog/09-coqide/12874-show_proof_diffs.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu.
+  See :ref:`showing_proof_diffs`.
+  (`#12874 <https://github.com/coq/coq/pull/12874>`_,
+  by Jim Fehrle and Enrico Tassi)
diff --git a/doc/sphinx/_static/diffs-show-proof.png b/doc/sphinx/_static/diffs-show-proof.png
new file mode 100644
index 0000000000..62bd9cccd0
--- /dev/null
+++ b/doc/sphinx/_static/diffs-show-proof.png
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index f90ebadb3a..f722ddda79 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -590,11 +590,11 @@ 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
+      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`.
+      It does not examine the :opt:`Diffs` option.  See :ref:`showing_proof_diffs`.
 
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
@@ -675,12 +675,9 @@ Requesting information
 Showing differences between proof steps
 ---------------------------------------
 
-
 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.
-
+and between values in some error messages.  Coq can also highlight differences
+in the proof term.
 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
@@ -826,14 +823,37 @@ the split because it has not changed.
   .. image:: ../_static/diffs-coqide-multigoal.png
      :alt: coqide with Set Diffs on with multiple goals
 
-This is how diffs may appear after applying a :tacn:`intro` tactic that results
-in compacted hypotheses:
+Diffs may appear like this after applying a :tacn:`intro` tactic that results
+in a compacted hypotheses:
 
 ..
 
   .. image:: ../_static/diffs-coqide-compacted.png
      :alt: coqide with Set Diffs on with compacted hypotheses
 
+.. _showing_proof_diffs:
+
+"Show Proof" differences
+````````````````````````
+
+To show differences in the proof term:
+
+- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command.
+
+- In CoqIDE, position the cursor on or just after a tactic to compare the proof term
+  after the tactic with the proof term before the tactic, then select
+  `View / Show Proof` from the menu or enter the associated key binding.
+  Differences will be shown applying the current `Show Diffs` setting
+  from the `View` menu.  If the current setting is `Don't show diffs`, diffs
+  will not be shown.
+
+  Output with the "added and removed" option looks like this:
+
+  ..
+
+    .. image:: ../_static/diffs-show-proof.png
+       :alt: coqide with Set Diffs on with compacted hypotheses
+
 Controlling the effect of proof editing commands
 ------------------------------------------------
 
diff --git a/ide/.merlin.in b/ide/.merlin.in
index b8d7953833..50816ae3f5 100644
--- a/ide/.merlin.in
+++ b/ide/.merlin.in
@@ -1,8 +1,10 @@
 PKG unix laglgtk3 lablgtk3-sourceview3 
 
-S utils
-B utils
-S protocol
-B protocol
+S coqide/utils
+B coqide/utils
+S coqide/protocol
+B coqide/protocol
+S coqide/
+B coqide/
 
 REC
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
index 038c8b91a8..1167b8199e 100644
--- a/ide/coqide/coq.ml
+++ b/ide/coqide/coq.ml
@@ -512,6 +512,7 @@ let hints x = eval_call (Xmlprotocol.hints x)
 let search flags = eval_call (Xmlprotocol.search flags)
 let init x = eval_call (Xmlprotocol.init x)
 let stop_worker x = eval_call (Xmlprotocol.stop_worker x)
+let proof_diff x = eval_call (Xmlprotocol.proof_diff x)
 
 let break_coqtop coqtop workers =
   if coqtop.status = Busy then
@@ -579,6 +580,9 @@ struct
   let set (type a) (opt : a t) (v : a) =
     Hashtbl.replace current_state (opt_name opt) (opt_data opt v)
 
+  let get (type a) (opt : a t) =
+    Hashtbl.find current_state (opt_name opt)
+
   let reset () =
     let init_descr d = List.iter (fun o -> set o d.init) d.opts in
     List.iter init_descr bool_items;
diff --git a/ide/coqide/coq.mli b/ide/coqide/coq.mli
index 82df36c91c..aaaf14e4d0 100644
--- a/ide/coqide/coq.mli
+++ b/ide/coqide/coq.mli
@@ -127,6 +127,7 @@ val hints      : Interface.hints_sty      -> Interface.hints_rty query
 val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
 val search     : Interface.search_sty     -> Interface.search_rty query
 val init       : Interface.init_sty       -> Interface.init_rty query
+val proof_diff : Interface.proof_diff_sty -> Interface.proof_diff_rty query
 
 val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
 
@@ -144,6 +145,10 @@ sig
 
   val set : 'a t -> 'a -> unit
 
+  val get : 'a t -> Interface.option_value
+
+  val diff : string t
+
   val printing_unfocused: unit -> bool
 
   (** [enforce] transmits to coq the current option values.
diff --git a/ide/coqide/coqOps.ml b/ide/coqide/coqOps.ml
index 29ea3ce9ea..97076745a3 100644
--- a/ide/coqide/coqOps.ml
+++ b/ide/coqide/coqOps.ml
@@ -142,6 +142,7 @@ object
   method handle_reset_initial : unit task
   method raw_coq_query :
     route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
+  method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task
   method initialize : unit task
@@ -361,6 +362,27 @@ object(self)
     let query = Coq.query (route_id,(phrase,sid)) in
     Coq.bind (Coq.seq action query) next
 
+  method proof_diff where ~next : unit Coq.task =
+    (* todo: would be nice to ignore comments, too *)
+    let rec back iter =
+      if iter#is_start then iter
+      else
+        let c = iter#char in
+        if Glib.Unichar.isspace c || c = 0 then back (iter#backward_char)
+        else if c = int_of_char '.' then iter#backward_char
+        else iter in
+
+    let where = back (buffer#get_iter_at_mark where) in
+    let until _ start stop =
+      (buffer#get_iter_at_mark stop)#compare where >= 0 &&
+      (buffer#get_iter_at_mark start)#compare where <= 0 in
+    let state_id = fst @@ self#find_id until in
+      let diff_opt = Interface.(match Coq.PrintOpt.(get diff) with
+        | StringValue diffs -> diffs
+        | _ -> "off") in
+      let proof_diff = Coq.proof_diff (diff_opt, state_id) in
+      Coq.bind proof_diff next
+
   method private still_valid { edit_id = id } =
     try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true
     with Not_found -> false
diff --git a/ide/coqide/coqOps.mli b/ide/coqide/coqOps.mli
index 3a4678ae9c..84911a6aa8 100644
--- a/ide/coqide/coqOps.mli
+++ b/ide/coqide/coqOps.mli
@@ -20,6 +20,7 @@ object
   method handle_reset_initial : unit task
   method raw_coq_query :
     route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
+  method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task
   method initialize : unit task
@@ -30,7 +31,6 @@ object
   method get_errors : (int * string) list
   method get_slaves_status : int * int * string CString.Map.t
 
-
   method handle_failure : handle_exn_rty -> unit task
 
   method destroy : unit -> unit
diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml
index b66da11e7b..f9e6e74372 100644
--- a/ide/coqide/coqide.ml
+++ b/ide/coqide/coqide.ml
@@ -747,6 +747,24 @@ let coq_icon () =
   let dir = List.find chk (Minilib.coqide_data_dirs ()) in
   Filename.concat dir name
 
+let show_proof_diff where sn =
+  sn.messages#default_route#clear;
+  Coq.try_grab sn.coqtop (sn.coqops#proof_diff where
+    ~next:(function
+        | Interface.Fail (_, _, err) ->
+            let err = if (Pp.string_of_ppcmds err) <> "No proofs to diff." then err else
+              Pp.str "Put the cursor over proven lines for \"Show Proof\" diffs"
+            in
+            let err = Ideutils.validate err in
+            sn.messages#default_route#add err;
+            Coq.return ()
+        | Interface.Good diff ->
+            sn.messages#default_route#add diff;
+            Coq.return ()))
+  ignore
+
+let show_proof_diffs _ = cb_on_current_term (show_proof_diff `INSERT) ()
+
 let about _ =
   let dialog = GWindow.about_dialog () in
   let _ = dialog#connect#response ~callback:(fun _ -> dialog#destroy ()) in
@@ -1103,6 +1121,8 @@ let build_ui () =
         radio "Set diff" 1 ~label:"Show diffs: only _added";
         radio "Set removed diff" 2 ~label:"Show diffs: added and _removed";
       ];
+    item "Show Proof Diffs" ~label:"_Show Proof (with diffs, if set)" ~accel:(modifier_for_display#get ^ "S")
+      ~callback:MiscMenu.show_proof_diffs;
   ];
   toggle_items view_menu Coq.PrintOpt.bool_items;
 
@@ -1352,6 +1372,11 @@ let main files =
     this default coqtop path *)
 
 let read_coqide_args argv =
+  let set_debug () =
+    Minilib.debug := true;
+    Flags.debug := true;
+    Exninfo.record_backtrace true
+  in
   let rec filter_coqtop coqtop project_files bindings_files out = function
     |"-unicode-bindings" :: sfilenames :: args ->
       let filenames = Str.split (Str.regexp ",") sfilenames in
@@ -1371,10 +1396,12 @@ let read_coqide_args argv =
     |"-coqtop" :: [] ->
       output_string stderr "Error: missing argument after -coqtop"; exit 1
     |"-debug"::args ->
-      Minilib.debug := true;
-      Flags.debug := true;
-      Exninfo.record_backtrace true;
+      set_debug ();
       filter_coqtop coqtop project_files bindings_files ("-debug"::out) args
+    |"-xml-debug"::args ->
+      set_debug ();
+      Flags.xml_debug := true;
+      filter_coqtop coqtop project_files bindings_files ("-xml-debug"::out) args
     |"-coqtop-flags" :: flags :: args->
       Coq.ideslave_coqtop_flags := Some flags;
       filter_coqtop coqtop project_files bindings_files out args
diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml
index e9ff1bbba1..6540fc6fca 100644
--- a/ide/coqide/coqide_ui.ml
+++ b/ide/coqide/coqide_ui.ml
@@ -89,6 +89,7 @@ let init () =
 \n    <menuitem action='Unset diff' />\
 \n    <menuitem action='Set diff' />\
 \n    <menuitem action='Set removed diff' />\
+\n    <menuitem action='Show Proof Diffs' />\
 \n  </menu>\
 \n  <menu action='Navigation'>\
 \n    <menuitem action='Forward' />\
diff --git a/ide/coqide/fake_ide.ml b/ide/coqide/fake_ide.ml
index e1736a5fe0..034f5b4e2a 100644
--- a/ide/coqide/fake_ide.ml
+++ b/ide/coqide/fake_ide.ml
@@ -136,7 +136,7 @@ module Parser = struct (* {{{ *)
     match g with
     | Item (s,_) -> Printf.sprintf "%s" (clean s)
     | Opt g -> Printf.sprintf "[%s]" (print g)
-    | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs))
+    | Alt gs -> Printf.sprintf "( %s )" (String.concat "\n| " (List.map print gs))
     | Seq gs -> String.concat " " (List.map print gs)
 
   let rec print_toklist = function
@@ -253,6 +253,9 @@ let eval_print l coq =
       after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
   | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
       eval_call (query (0,(phrase,tip_id()))) coq
+  | [ Tok(_,"PDIFF"); Tok(_,id) ] ->
+      let to_id, _ = get_id id in
+      eval_call (proof_diff ("on",to_id)) coq
   | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
       let to_id, _ = get_id id in
       eval_call (query (0,(phrase, to_id))) coq
@@ -282,6 +285,7 @@ let grammar =
     ; Seq [Item (eat_rex "FAILADD"); Item eat_phrase]
     ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
     ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
+    ; Seq [Item (eat_rex "PDIFF");  Item eat_id ]
     ; Seq [Item (eat_rex "WAIT")]
     ; Seq [Item (eat_rex "JOIN")]
     ; Seq [Item (eat_rex "GOALS")]
@@ -295,12 +299,11 @@ let grammar =
 let read_command inc = Parser.parse grammar inc
 
 let usage () =
-  error (Printf.sprintf
-    "A fake coqide process talking to a coqtop -toploop coqidetop.\n\
-     Usage: %s (file|-) [<coqtop>]\n\
-     Input syntax is the following:\n%s\n"
-     (Filename.basename Sys.argv.(0))
-     (Parser.print grammar))
+  prerr_endline (Printf.sprintf "Usage: %s ( file | - ) [ \"<coqtop arguments>\" ]\n\
+    Input syntax is:\n%s\n"
+    (Filename.basename Sys.argv.(0))
+    (Parser.print grammar));
+  exit 1
 
 module Coqide = Spawn.Sync ()
 
@@ -308,14 +311,15 @@ let main =
   if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
-  let def_args = ["--xml_format=Ppcmds"] in
   let idetop_name = System.get_toplevel_path "coqidetop" in
-  let coqtop_args, input_file = match Sys.argv with
-    | [| _; f |] -> Array.of_list def_args, f
-    | [| _; f; ct |] ->
-        let ct = Str.split (Str.regexp " ") ct in
-        Array.of_list (def_args @ ct), f
+  let input_file, args  = match Sys.argv with
+    | [| _; f |] -> f, []
+    | [| _; f; args |] ->
+        let args = Str.split (Str.regexp " ") args in
+        f, args
     | _ -> usage () in
+  let def_coqtop_args = ["--xml_format=Ppcmds"] in
+  let coqtop_args = Array.of_list(def_coqtop_args @ args) in
   let inc = if input_file = "-" then stdin else open_in input_file in
   prerr_endline ("Running: "^idetop_name^" "^
                    (String.concat " " (Array.to_list coqtop_args)));
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index ad21f663e4..297dc3a706 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -367,6 +367,17 @@ let export_option_state s = {
   Interface.opt_value = export_option_value s.Goptions.opt_value;
 }
 
+exception NotSupported of string
+
+let proof_diff (diff_opt, sid) =
+  let diff_opt = Proof_diffs.string_to_diffs diff_opt in
+  let doc = get_doc () in
+  match Stm.get_proof ~doc sid with
+  | None -> CErrors.user_err (Pp.str "No proofs to diff.")
+  | Some proof ->
+      let old = Stm.get_prev_proof ~doc sid in
+      Proof_diffs.diff_proofs ~diff_opt ?old proof
+
 let get_options () =
   let table = Goptions.get_tables () in
   let fold key state accu = (key, export_option_state state) :: accu in
@@ -455,6 +466,7 @@ let eval_call c =
     Interface.hints = interruptible hints;
     Interface.status = interruptible status;
     Interface.search = interruptible search;
+    Interface.proof_diff = interruptible proof_diff;
     Interface.get_options = interruptible get_options;
     Interface.set_options = interruptible set_options;
     Interface.mkcases = interruptible idetop_make_cases;
@@ -479,6 +491,8 @@ let print_xml =
   let m = Mutex.create () in
   fun oc xml ->
     Mutex.lock m;
+    if !Flags.xml_debug then
+      Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml);
     try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m
     with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e
 
@@ -507,7 +521,7 @@ let loop run_mode ~opts:_ state =
   set_doc state.doc;
   init_signal_handler ();
   catch_break := false;
-  let in_ch, out_ch = Spawned.get_channels ()                        in
+  let in_ch, out_ch = Spawned.get_channels () in
   let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in
   let in_lb         = Lexing.from_function (fun s len ->
                       CThread.thread_friendly_read in_ch s ~off:0 ~len) in
@@ -518,7 +532,8 @@ let loop run_mode ~opts:_ state =
   while not !quit do
     try
       let xml_query = Xml_parser.parse xml_ic in
-(*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
+      if !Flags.xml_debug then
+        pr_with_pid (Xml_printer.to_string_fmt xml_query);
       let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
       let r  = eval_call q in
diff --git a/ide/coqide/protocol/interface.ml b/ide/coqide/protocol/interface.ml
index 646012dcaa..86a81446e8 100644
--- a/ide/coqide/protocol/interface.ml
+++ b/ide/coqide/protocol/interface.ml
@@ -187,6 +187,10 @@ type status_rty = status
 type search_sty = search_flags
 type search_rty = string coq_object list
 
+(** Diffs between the proof term at a given stateid and the previous one *)
+type proof_diff_sty = string * Stateid.t
+type proof_diff_rty = Pp.t
+
 (** Retrieve the list of options of the current toplevel *)
 type get_options_sty = unit
 type get_options_rty = (option_name * option_state) list
@@ -252,6 +256,7 @@ type handler = {
   stop_worker : stop_worker_sty -> stop_worker_rty;
   print_ast   : print_ast_sty   -> print_ast_rty;
   annotate    : annotate_sty    -> annotate_rty;
+  proof_diff  : proof_diff_sty  -> proof_diff_rty;
   handle_exn  : handle_exn_sty  -> handle_exn_rty;
   init        : init_sty        -> init_rty;
   quit        : quit_sty        -> quit_rty;
diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml
index 9e861baac6..6a33ff8abc 100644
--- a/ide/coqide/protocol/xmlprotocol.ml
+++ b/ide/coqide/protocol/xmlprotocol.ml
@@ -12,7 +12,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20170413"
+let protocol_version = "20200911"
 
 type msg_format = Richpp of int | Ppcmds
 let msg_format = ref (Richpp 72)
@@ -278,6 +278,7 @@ module ReifType : sig
   val state_id_t     : state_id val_t
   val route_id_t     : route_id val_t
   val search_cst_t   : search_constraint val_t
+  val pp_t           : Pp.t val_t
 
   val of_value_type : 'a val_t -> 'a -> xml
   val to_value_type : 'a val_t -> xml -> 'a
@@ -314,6 +315,7 @@ end = struct
     | State_id : state_id val_t
     | Route_id : route_id val_t
     | Search_cst : search_constraint val_t
+    | Pp : Pp.t val_t
 
   type value_type = Value_type : 'a val_t -> value_type
 
@@ -340,6 +342,7 @@ end = struct
   let state_id_t     = State_id
   let route_id_t     = Route_id
   let search_cst_t   = Search_cst
+  let pp_t           = Pp
 
   let of_value_type (ty : 'a val_t) : 'a -> xml =
     let rec convert : type a. a val_t -> a -> xml = function
@@ -362,6 +365,7 @@ end = struct
       | State_id      -> of_stateid
       | Route_id      -> of_routeid
       | Search_cst    -> of_search_cst
+      | Pp            -> of_pp
     in
       convert ty
 
@@ -386,6 +390,7 @@ end = struct
       | State_id      -> to_stateid
       | Route_id      -> to_routeid
       | Search_cst    -> to_search_cst
+      | Pp            -> to_pp
     in
       convert ty
 
@@ -443,6 +448,8 @@ end = struct
     | In_Module s -> "In_Module " ^ String.concat "." s
     | Include_Blacklist -> "Include_Blacklist"
 
+  let pr_pp = Pp.string_of_ppcmds
+
   let rec print : type a. a val_t -> a -> string = function
   | Unit          -> pr_unit
   | Bool          -> pr_bool
@@ -463,6 +470,7 @@ end = struct
   | Union (t1,t2) -> (pr_union (print t1) (print t2))
   | State_id      -> pr_state_id
   | Route_id      -> pr_int
+  | Pp            -> pr_pp
 
   (* This is to break if a rename/refactoring makes the strings below outdated *)
   type 'a exists = bool
@@ -489,6 +497,7 @@ end = struct
                      Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2)
   | State_id      -> assert(true : Stateid.t exists); "Stateid.t"
   | Route_id      -> assert(true : route_id exists); "route_id"
+  | Pp            -> assert(true : Pp.t exists); "Pp.t"
 
   let print_type = function Value_type ty -> print_val_t ty
 
@@ -507,6 +516,8 @@ end = struct
       (pr_xml (of_pair of_bool of_int (false,3)));
     Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int)))
       (pr_xml (of_union of_bool of_int (Inl false)));
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t Pp)
+      (pr_xml (of_pp Pp.(hv 3 (str "foo" ++ spc () ++ str "bar") )));
     print_endline ("All other types are records represented by a node named like the OCaml\n"^
                    "type which contains a flattened n-tuple.  We provide one example.\n");
     Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
@@ -538,6 +549,7 @@ let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
 let stop_worker_sty_t : stop_worker_sty val_t = string_t
 let print_ast_sty_t : print_ast_sty val_t = state_id_t
 let annotate_sty_t : annotate_sty val_t = string_t
+let proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t
 
 let add_rty_t : add_rty val_t =
   pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
@@ -563,6 +575,7 @@ let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string
 let stop_worker_rty_t : stop_worker_rty val_t = unit_t
 let print_ast_rty_t : print_ast_rty val_t = xml_t
 let annotate_rty_t : annotate_rty val_t = xml_t
+let proof_diff_rty_t : proof_diff_rty val_t = pp_t
 
 let ($) x = erase x
 let calls = [|
@@ -585,6 +598,7 @@ let calls = [|
   "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t;
   "PrintAst",   ($)print_ast_sty_t,   ($)print_ast_rty_t;
   "Annotate",   ($)annotate_sty_t,    ($)annotate_rty_t;
+  "PDiff",      ($)proof_diff_sty_t,  ($)proof_diff_rty_t;
 |]
 
 type 'a call =
@@ -609,7 +623,9 @@ type 'a call =
   | Interp     : interp_sty -> interp_rty call
   | PrintAst   : print_ast_sty -> print_ast_rty call
   | Annotate   : annotate_sty -> annotate_rty call
+  | PDiff      : proof_diff_sty -> proof_diff_rty call
 
+(* the order of the entries must match the order in "calls" above *)
 let id_of_call : type a. a call -> int = function
   | Add _        -> 0
   | Edit_at _    -> 1
@@ -630,6 +646,7 @@ let id_of_call : type a. a call -> int = function
   | StopWorker _ -> 16
   | PrintAst _   -> 17
   | Annotate _   -> 18
+  | PDiff _     -> 19
 
 let str_of_call c = pi1 calls.(id_of_call c)
 
@@ -652,8 +669,9 @@ let init x        : init_rty call        = Init x
 let wait x        : wait_rty call        = Wait x
 let interp x      : interp_rty call      = Interp x
 let stop_worker x : stop_worker_rty call = StopWorker x
-let print_ast   x : print_ast_rty call   = PrintAst x
-let annotate   x : annotate_rty call    = Annotate x
+let print_ast x   : print_ast_rty call   = PrintAst x
+let annotate x    : annotate_rty call    = Annotate x
+let proof_diff x  : proof_diff_rty call  = PDiff x
 
 let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
   let mkGood : type a. a -> a value = fun x -> Good x in
@@ -678,6 +696,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
     | StopWorker x -> mkGood (handler.stop_worker x)
     | PrintAst x   -> mkGood (handler.print_ast x)
     | Annotate x   -> mkGood (handler.annotate x)
+    | PDiff x      -> mkGood (handler.proof_diff x)
   with any ->
     let any = Exninfo.capture any in
     Fail (handler.handle_exn any)
@@ -703,6 +722,7 @@ let of_answer : type a. a call -> a value -> xml = function
   | StopWorker _ -> of_value (of_value_type stop_worker_rty_t)
   | PrintAst _   -> of_value (of_value_type print_ast_rty_t  )
   | Annotate _   -> of_value (of_value_type annotate_rty_t   )
+  | PDiff _      -> of_value (of_value_type proof_diff_rty_t )
 
 let of_answer msg_fmt =
   msg_format := msg_fmt; of_answer
@@ -727,6 +747,7 @@ let to_answer : type a. a call -> xml -> a value = function
   | StopWorker _ -> to_value (to_value_type stop_worker_rty_t)
   | PrintAst _   -> to_value (to_value_type print_ast_rty_t  )
   | Annotate _   -> to_value (to_value_type annotate_rty_t   )
+  | PDiff _      -> to_value (to_value_type proof_diff_rty_t )
 
 let of_call : type a. a call -> xml = fun q ->
   let mkCall x = constructor "call" (str_of_call q) [x] in
@@ -750,6 +771,7 @@ let of_call : type a. a call -> xml = fun q ->
   | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x)
   | PrintAst x   -> mkCall (of_value_type print_ast_sty_t   x)
   | Annotate x   -> mkCall (of_value_type annotate_sty_t    x)
+  | PDiff x      -> mkCall (of_value_type proof_diff_sty_t  x)
 
 let to_call : xml -> unknown_call =
   do_match "call" (fun s a ->
@@ -774,6 +796,7 @@ let to_call : xml -> unknown_call =
     | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a))
     | "PrintAst"   -> Unknown (PrintAst   (mkCallArg print_ast_sty_t   a))
     | "Annotate"   -> Unknown (Annotate   (mkCallArg annotate_sty_t    a))
+    | "PDiff"      -> Unknown (PDiff      (mkCallArg proof_diff_sty_t  a))
     | x -> raise (Marshal_error("call",PCData x)))
 
 (** Debug printing *)
@@ -805,6 +828,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc
   | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value
   | PrintAst _   -> pr_value_gen (print print_ast_rty_t  ) value
   | Annotate _   -> pr_value_gen (print annotate_rty_t   ) value
+  | PDiff _      -> pr_value_gen (print proof_diff_rty_t ) value
 let pr_call : type a. a call -> string = fun call ->
   let return what x = str_of_call call ^ " " ^ print what x in
   match call with
@@ -827,6 +851,7 @@ let pr_call : type a. a call -> string = fun call ->
     | StopWorker x -> return stop_worker_sty_t x
     | PrintAst x   -> return print_ast_sty_t x
     | Annotate x   -> return annotate_sty_t x
+    | PDiff x      -> return proof_diff_sty_t x
 
 let document to_string_fmt =
   Printf.printf "=== Available calls ===\n\n";
diff --git a/ide/coqide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli
index 44584d44d7..4dc05c18a9 100644
--- a/ide/coqide/protocol/xmlprotocol.mli
+++ b/ide/coqide/protocol/xmlprotocol.mli
@@ -37,6 +37,7 @@ val wait        : wait_sty        -> wait_rty call
 val interp      : interp_sty      -> interp_rty call
 val print_ast   : print_ast_sty   -> print_ast_rty call
 val annotate    : annotate_sty    -> annotate_rty call
+val proof_diff  : proof_diff_sty  -> proof_diff_rty call
 
 val abstract_eval_call : handler -> 'a call -> 'a value
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 1d9d6d49bc..83733cf00d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 let load_vos_libraries = ref false
 
 let debug = ref false
+let xml_debug = ref false
 
 let in_debugger = ref false
 let in_toplevel = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 30d1b5b2bd..ebd23a4d20 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -41,6 +41,7 @@ val load_vos_libraries : bool ref
 
 (** Debug flags *)
 val debug : bool ref
+val xml_debug : bool ref
 val in_debugger : bool ref
 val in_toplevel : bool ref
 
diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml
index 988e8e4303..4593bf4b07 100644
--- a/lib/pp_diff.ml
+++ b/lib/pp_diff.ml
@@ -109,7 +109,7 @@ let shorten_diff_span dtype diff_list =
 
   iter 0 len (<) 1; (* left to right *)
   iter (len-1) (-1) (>) (-1); (* right to left *)
-  if !changed then Array.to_list diffs else diff_list;;
+  if !changed then Array.to_list diffs else diff_list
 
 let has_changes diffs =
   let rec has_changes_r diffs added removed =
@@ -118,12 +118,12 @@ let has_changes diffs =
     | `Removed _ :: t -> has_changes_r t added true
     | h :: t -> has_changes_r t added removed
     | [] -> (added, removed) in
-  has_changes_r diffs false false;;
+  has_changes_r diffs false false
 
 (* get the Myers diff of 2 lists of strings *)
 let diff_strs old_strs new_strs =
   let diffs = List.rev (StringDiff.diff old_strs new_strs) in
-  shorten_diff_span `Removed (shorten_diff_span `Added diffs);;
+  shorten_diff_span `Removed (shorten_diff_span `Added diffs)
 
 (* Default string tokenizer.  Makes each character a separate strin.
 Whitespace is not ignored.  Doesn't handle UTF-8 differences well. *)
@@ -139,7 +139,7 @@ let def_tokenize_string s =
 let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str =
   let old_toks = Array.of_list (tokenize_string old_str)
   and new_toks = Array.of_list (tokenize_string new_str) in
-  diff_strs old_toks new_toks;;
+  diff_strs old_toks new_toks
 
 let get_dinfo = function
   | `Common (_, _, s) -> (`Common, s)
@@ -281,14 +281,14 @@ let add_diff_tags which pp diffs  =
   skip ();
   if !diffs <> [] then
     raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible");
-  if has_added || has_removed then wrap_in_bg diff_tag rv else rv;;
+  if has_added || has_removed then wrap_in_bg diff_tag rv else rv
 
 let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp =
   let open Pp in
   let o_str = string_of_ppcmds o_pp in
   let n_str = string_of_ppcmds n_pp in
   let diffs = diff_str ~tokenize_string o_str n_str in
-  (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);;
+  (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs)
 
 let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp =
   let open Pp in
@@ -300,4 +300,4 @@ let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false
   if show_removed && has_removed then
     let removed = add_diff_tags `Removed o_pp diffs in
     (v 0 (removed ++ cut() ++ added))
-  else added;;
+  else added
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
diff --git a/test-suite/ide/proof-diffs.fake b/test-suite/ide/proof-diffs.fake
new file mode 100644
index 0000000000..594ebced23
--- /dev/null
+++ b/test-suite/ide/proof-diffs.fake
@@ -0,0 +1,10 @@
+ADD { Goal True /\ False /\ True = False. }
+ADD { split. }
+GOALS
+ADD here { split. }
+GOALS
+PDIFF here
+ADD there { auto. }
+GOALS
+PDIFF there
+ADD { Admitted. }
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\