From 829a8feb3d02da057d39b5029b422e8a45dd1608 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 25 Jan 2017 14:39:29 +0100
Subject: [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`
---
 ide/ide_slave.ml | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

(limited to 'ide/ide_slave.ml')

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"
-- 
cgit v1.2.3