[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`

9 files changed, 51 insertions, 16 deletions

diff --git a/Makefile.build b/Makefile.build
index 3b8d82e68..01cc4d878 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -442,7 +442,7 @@ $(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkm
 
 FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo	ide/document.cmo \
  ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \
- ide/xmlprotocol.cmo tools/fake_ide.cmo
+ ide/richpp.cmo ide/xmlprotocol.cmo tools/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
diff --git a/ide/coq.ml b/ide/coq.ml
index bb9d6e522..3a1d87787 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 12170c462..78b4c01e8 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 2065a4546..db450b4bc 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 1d50aed03..b4f2ad0be 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 43a65dfa8..9cefab517 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
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 4b254e811..72b538016 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -5,6 +5,7 @@ TQueue
 WorkerPool
 Vernac_classifier
 CoqworkmgrApi
+WorkerLoop
 AsyncTaskQueue
 Stm
 ProofBlockDelimiter
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
index 56fcf8537..50b42512c 100644
--- a/stm/workerLoop.ml
+++ b/stm/workerLoop.ml
@@ -6,9 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let rec parse args = args
+let rec parse = function
+  | "--xml_format=Ppcmds" :: rest -> parse rest
+  | x :: rest -> x :: parse rest
+  | [] -> []
 
 let loop init args =
+  let args = parse args in
   Flags.make_silent true;
   init ();
   CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 7a891239b..932097607 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -296,11 +296,12 @@ let main =
   Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
+  let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
   let coqtop_name, coqtop_args, input_file = match Sys.argv with
-    | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+    | [| _; f |] -> "coqtop", Array.of_list def_args, f
     | [| _; f; ct |] ->
         let ct = Str.split (Str.regexp " ") ct in
-        List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
+        List.hd ct, Array.of_list (def_args @ List.tl ct), f
     | _ -> usage () in
   let inc = if input_file = "-" then stdin else open_in input_file in
   let coq =