aboutsummaryrefslogtreecommitdiff
path: root/ide/xmlprotocol.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-01-25 14:39:29 +0100
committerEmilio Jesus Gallego Arias2017-03-21 15:51:49 +0100
commit829a8feb3d02da057d39b5029b422e8a45dd1608 (patch)
treed2caa3d95e3c5462125c54745ed56ba924664dd6 /ide/xmlprotocol.ml
parent6e3fc0992be7ddd841328028dec51d390fffb851 (diff)
[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`
Diffstat (limited to 'ide/xmlprotocol.ml')
-rw-r--r--ide/xmlprotocol.ml17
1 files changed, 17 insertions, 0 deletions
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);