diff options
| author | Maxime Dénès | 2017-03-22 14:09:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-22 14:09:41 +0100 |
| commit | 6e0ca299c407125a8d65f54ab424bdae3667125e (patch) | |
| tree | 2f968c31b85b22190d4ce9f2472f4cb6cd0a6ad9 /ide/xmlprotocol.mli | |
| parent | 051ef20a9f9c496fc6a5143de97450ccf7786c5b (diff) | |
| parent | aa9e94275ccac92311a6bdac563b61a6c7876cec (diff) | |
Merge PR#390: Updates to the Pretty Printing Infrastructure
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 1bb9989704..9cefab517f 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 |