diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-01 16:51:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-02 16:45:39 +0200 |
| commit | ffd89ea323937b7d323e24a2b6d53cdc857117dd (patch) | |
| tree | 0e2a089a429486362bf5a4cd00e7662dee450a11 /lib/feedback.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 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 20 |
1 files changed, 4 insertions, 16 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 1e96f9a49..50ffd22db 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -16,20 +16,12 @@ type level = | Warning | Error -type message = { - message_level : level; - message_content : xml; -} - -val of_message : message -> xml -val to_message : xml -> message -val is_message : xml -> bool - (** Coq "semantic" infos obtained during parsing/execution *) type edit_id = int type state_id = Stateid.t type edit_or_state_id = Edit of edit_id | State of state_id + type route_id = int val default_route : route_id @@ -54,18 +46,14 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Old generic messages *) - | Message of message + | Message of level * Richpp.richpp type feedback = { - id : edit_or_state_id; (* The document part concerned *) + id : edit_or_state_id; (* The document part concerned *) contents : feedback_content; (* The payload *) - route : route_id; (* Extra routing info *) + route : route_id; (* Extra routing info *) } -val of_feedback : feedback -> xml -val to_feedback : xml -> feedback -val is_feedback : xml -> bool - (** {6 Feedback sent, even asynchronously, to the user interface} *) (** Moved here from pp.ml *) |