diff options
Diffstat (limited to 'ide/xmlprotocol.mli')
| -rw-r--r-- | ide/xmlprotocol.mli | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 1bb998970..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 *) @@ -57,16 +62,8 @@ val pr_call : 'a call -> string val pr_value : 'a value -> string val pr_full_value : 'a call -> 'a value -> string -(** * Serialization of rich documents *) -val of_richpp : Richpp.richpp -> Xml_datatype.xml -val to_richpp : Xml_datatype.xml -> Richpp.richpp - (** * 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 is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option -val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml -(* val to_message : xml -> Feedback.message *) +val is_feedback : xml -> bool |