diff options
| author | Pierre-Marie Pédrot | 2016-06-02 18:00:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-02 18:00:30 +0200 |
| commit | 71b64cc5ec5ab0d70d437ec4542c5903f43063cb (patch) | |
| tree | 440fb8e51d1fe118d866d0c620a86724e3c6eae8 /ide/xmlprotocol.mli | |
| parent | 2d2d86c165cac7b051da1c5079d614a76550a20c (diff) | |
| parent | 318fc2c04df1e73cc8a178d4fc1ce8bf5543649b (diff) | |
Move XML serialization to ide/ folder.
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 *) + |