From ffd89ea323937b7d323e24a2b6d53cdc857117dd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 1 Jun 2016 16:51:15 +0200
Subject: 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.
---
 lib/feedback.mli | 20 ++++----------------
 1 file changed, 4 insertions(+), 16 deletions(-)

(limited to 'lib/feedback.mli')

diff --git a/lib/feedback.mli b/lib/feedback.mli
index 1e96f9a497..50ffd22db9 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 *)
-- 
cgit v1.2.3