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.

1 files changed, 8 insertions, 8 deletions

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d5ef807b6..221fb36d8 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -28,7 +28,8 @@ let error_xml s =
   Printf.eprintf "fake_id: error: %a\n%!" print_xml s;
   exit 1
 
-let logger level content = Printf.eprintf "%a\n%! " print_xml content
+let logger level content =
+  Printf.eprintf "%a\n%! " print_xml (Richpp.repr content)
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -36,15 +37,14 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
-    if Feedback.is_message xml then
-      let message = Feedback.to_message xml in
-      let level = message.Feedback.message_level in
-      let content = message.Feedback.message_content in
+    match Xmlprotocol.is_message xml with
+    | Some (level, content) ->
       logger level content;
       loop ()
-    else if Feedback.is_feedback xml then
-      loop ()
-    else (Xmlprotocol.to_answer call xml)
+    | None ->
+      if Xmlprotocol.is_feedback xml then
+        loop ()
+      else Xmlprotocol.to_answer call xml
   in
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);