[xml] Restore protocol compatibility with 8.6.

By default, we serialize messages to the "rich printing
representation" as it was done in 8.6, this ways clients don't have to
adapt unless they specifically request the new format using option
`--xml_format=Ppcmds`

5 files changed, 41 insertions, 12 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index bb9d6e5228..3a1d877872 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -366,7 +366,7 @@ let bind_self_as f =
 (** This launches a fresh handle from its command line arguments. *)
 let spawn_handle args respawner feedback_processor =
   let prog = coqtop_path () in
-  let args = Array.of_list ("-async-proofs" :: "on" :: "-ideslave" :: args) in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
   let env =
     match !Flags.ideslave_coqtop_flags with
     | None -> None
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 12170c4621..78b4c01e8c 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -14,6 +14,7 @@ Xml_parser
 Xml_printer
 Serialize
 Richpp
+Topfmt
 Xmlprotocol
 Ideutils
 Coq
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 2065a45467..db450b4bc8 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -441,8 +441,8 @@ let print_xml =
     try Xml_printer.print oc xml; Mutex.unlock m
     with e -> let e = CErrors.push e in Mutex.unlock m; iraise e
 
-let slave_feeder xml_oc msg =
-  let xml = Xmlprotocol.of_feedback msg in
+let slave_feeder fmt xml_oc msg =
+  let xml = Xmlprotocol.(of_feedback fmt msg) in
   print_xml xml_oc xml
 
 (** The main loop *)
@@ -451,6 +451,11 @@ let slave_feeder xml_oc msg =
     messages by [handle_exn] above. Otherwise, we die badly, without
     trying to answer malformed requests. *)
 
+let msg_format = ref (fun () ->
+    let margin = Option.default 72 (Topfmt.get_margin ()) in
+    Xmlprotocol.Richpp margin
+)
+
 let loop () =
   init_signal_handler ();
   catch_break := false;
@@ -461,7 +466,7 @@ let loop () =
   (* SEXP parser make *)
   let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
-  Feedback.add_feeder (slave_feeder xml_oc);
+  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -474,7 +479,7 @@ let loop () =
       let r  = eval_call q in
       let () = pr_debug_answer q r in
 (*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
-      print_xml xml_oc (Xmlprotocol.of_answer q r);
+      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);
       flush out_ch
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->
@@ -496,6 +501,8 @@ let loop () =
 let rec parse = function
   | "--help-XML-protocol" :: rest ->
         Xmlprotocol.document Xml_printer.to_string_fmt; exit 0
+  | "--xml_format=Ppcmds" :: rest ->
+        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest
   | x :: rest -> x :: parse rest
   | [] -> []
 
@@ -507,4 +514,6 @@ let () = Coqtop.toploop_init := (fun args ->
 
 let () = Coqtop.toploop_run := loop
 
-let () = Usage.add_to_usage "coqidetop" "  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
+let () = Usage.add_to_usage "coqidetop"
+"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format
+  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 1d50aed032..b4f2ad0bef 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -12,6 +12,9 @@
 
 let protocol_version = "20150913"
 
+type msg_format = Richpp of int | Ppcmds
+let msg_format = ref (Richpp 72)
+
 (** * Interface of calls to Coq by CoqIde *)
 
 open Util
@@ -135,6 +138,14 @@ let rec to_pp xpp = let open Pp in
     | x           -> raise (Marshal_error("*ppdoc",PCData x))
   ) xpp
 
+let of_richpp x = Element ("richpp", [], [x])
+
+(* Run-time Selectable *)
+let of_pp (pp : Pp.std_ppcmds) =
+  match !msg_format with
+  | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp)
+  | Ppcmds        -> of_pp pp
+
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
 | Fail (id,loc, msg) ->
@@ -669,6 +680,9 @@ let of_answer : type a. a call -> a value -> xml = function
   | PrintAst _   -> of_value (of_value_type print_ast_rty_t  )
   | Annotate _   -> of_value (of_value_type annotate_rty_t   )
 
+let of_answer msg_fmt =
+  msg_format := msg_fmt; of_answer
+
 let to_answer : type a. a call -> xml -> a value = function
   | Add _        -> to_value (to_value_type add_rty_t        )
   | Edit_at _    -> to_value (to_value_type edit_at_rty_t    )
@@ -902,6 +916,9 @@ let of_feedback msg =
   let route = string_of_int msg.route in
   Element ("feedback", obj @ ["route",route], [id;content])
 
+let of_feedback msg_fmt =
+  msg_format := msg_fmt; of_feedback
+
 let to_feedback xml = match xml with
   | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
       id = Edit(to_edit_id id);
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 43a65dfa85..9cefab517f 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -40,12 +40,17 @@ val abstract_eval_call : handler -> 'a call -> 'a value
 
 val protocol_version : string
 
+(** By default, we still output messages in Richpp so we are
+    compatible with 8.6, however, 8.7 aware clients will want to
+    set this to Ppcmds *)
+type msg_format = Richpp of int | Ppcmds
+
 (** * XML data marshalling *)
 
 val of_call : 'a call -> xml
 val to_call : xml -> unknown_call
 
-val of_answer : 'a call -> 'a value -> xml
+val of_answer : msg_format -> 'a call -> 'a value -> xml
 val to_answer : 'a call -> xml -> 'a value
 
 (* Prints the documentation of this module *)
@@ -58,10 +63,7 @@ val pr_value : 'a value -> string
 val pr_full_value : 'a call -> 'a value -> string
 
 (** * Serializaiton of feedback  *)
-val of_feedback : Feedback.feedback -> xml
+val of_feedback : msg_format -> Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback
-val is_feedback : xml -> bool
-
-val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml
-(* val to_message : xml -> Feedback.message *)
 
+val is_feedback : xml -> bool