diff options
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 17 |
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); |