Add an XML message for "Show Proof Diffs"

Add menu item that uses this

11 files changed, 131 insertions, 22 deletions

diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
index 57cdccce6d..6e5d57c9a5 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
@@ -578,6 +579,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 2adc35ae3e..2be8f862ea 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 6cb0cec008..0780f03903 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