diff options
| author | Emilio Jesus Gallego Arias | 2017-01-25 14:39:29 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:49 +0100 |
| commit | 829a8feb3d02da057d39b5029b422e8a45dd1608 (patch) | |
| tree | d2caa3d95e3c5462125c54745ed56ba924664dd6 /ide/xmlprotocol.mli | |
| parent | 6e3fc0992be7ddd841328028dec51d390fffb851 (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.mli')
| -rw-r--r-- | ide/xmlprotocol.mli | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 43a65dfa85..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 *) @@ -58,10 +63,7 @@ val pr_value : 'a value -> string val pr_full_value : 'a call -> 'a value -> string (** * 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 of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml -(* val to_message : xml -> Feedback.message *) +val is_feedback : xml -> bool |