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/xmlprotocol.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'ide/xmlprotocol.ml')

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