diff options
| author | Emilio Jesus Gallego Arias | 2016-06-01 16:51:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-06-02 16:45:39 +0200 |
| commit | ffd89ea323937b7d323e24a2b6d53cdc857117dd (patch) | |
| tree | 0e2a089a429486362bf5a4cd00e7662dee450a11 /ide/xmlprotocol.mli | |
| parent | e020cc70578b65609ac7337537f16a1c25254e77 (diff) | |
Encapsulate xml serialization in xmlprotocol.mli
This eases the task of replacing/improving the serializer, as well as
making it more resistant. See pitfalls below:
Main changes are:
- fold `message` type into `feedback` type
- make messages of type `Richpp.richpp` so we are explicit about the
content being a rich document.
- moved serialization functions for messages and stateid to `Xmlprotocol`
- improved a couple of internal API points (`is_message`).
Tested.
Diffstat (limited to 'ide/xmlprotocol.mli')
| -rw-r--r-- | ide/xmlprotocol.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 265a50c47c..6bca8772ed 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -56,3 +56,17 @@ val document : (xml -> string) -> unit 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 to_feedback : xml -> Feedback.feedback +val is_feedback : xml -> bool + +val is_message : xml -> (Feedback.level * Richpp.richpp) option +val of_message : Feedback.level -> Richpp.richpp -> xml +(* val to_message : xml -> Feedback.message *) + |