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.

11 files changed, 206 insertions, 216 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 7a32faffc..82fd48c9e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -290,12 +290,9 @@ let rec check_errors = function
 | `NVAL :: _ -> raise (TubeError "NVAL")
 | `OUT :: _ -> raise (TubeError "OUT")
 
-let handle_intermediate_message handle xml =
-  let message = Feedback.to_message xml in
-  let level = message.Feedback.message_level in
-  let content = message.Feedback.message_content in
-  let logger = match handle.waiting_for with
-    | Some (_, l) -> l 
+let handle_intermediate_message handle level content =
+  let logger  = match handle.waiting_for with
+    | Some (_, l) -> l
     | None -> function
         | Feedback.Error   -> fun s -> Minilib.log ~level:`ERROR   (xml_to_string s)
         | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
@@ -303,10 +300,10 @@ let handle_intermediate_message handle xml =
         | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
         | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
   in
-  logger level (Richpp.richpp_of_xml content)
+  logger level content
 
 let handle_feedback feedback_processor xml =
-  let feedback = Feedback.to_feedback xml in
+  let feedback = Xmlprotocol.to_feedback xml in
   feedback_processor feedback
 
 let handle_final_answer handle xml =
@@ -335,15 +332,18 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     let l_end = Lexing.lexeme_end lex in
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
-    if Feedback.is_message xml then begin
-      handle_intermediate_message handle xml;
+    match Xmlprotocol.is_message xml with
+    | Some (lvl, msg) ->
+      handle_intermediate_message handle lvl msg;
       loop ()
-    end else if Feedback.is_feedback xml then begin
-      handle_feedback feedback_processor xml;
-      loop ()
-    end else begin
-      ignore (handle_final_answer handle xml)
-    end
+    | None ->
+      if Xmlprotocol.is_feedback xml then begin
+        handle_feedback feedback_processor xml;
+        loop ()
+      end else
+        begin
+          ignore (handle_final_answer handle xml)
+        end
   in
   try loop ()
   with Xml_parser.Error _ as e ->
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 4b043661e..0e09d8409 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -453,16 +453,12 @@ let print_xml =
 let slave_logger xml_oc level message =
   (* convert the message into XML *)
   let msg = hov 0 message in
-  let message = {
-    Feedback.message_level = level;
-    Feedback.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
-  } in
-  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
-  let xml = Feedback.of_message message in
+  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))    in
+  let xml = Xmlprotocol.of_message level (Richpp.richpp_of_pp message) in
   print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
-  let xml = Feedback.of_feedback msg in
+  let xml = Xmlprotocol.of_feedback msg in
   print_xml xml_oc xml
 
 (** The main loop *)
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 232630e5b..45279a7c3 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -84,6 +84,18 @@ let to_option_state = function
       opt_value = to_option_value value }
   | _ -> raise Marshal_error
 
+let to_stateid = function
+  | Element ("state_id",["val",i],[]) ->
+      let id = int_of_string i in
+      Stateid.of_int id
+  | _ -> raise (Invalid_argument "to_state_id")
+
+let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[])
+
+let of_richpp x = Element ("richpp", [], [Richpp.repr x])
+let to_richpp xml = match xml with
+  | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x
+  | _ -> raise Serialize.Marshal_error
 
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
@@ -91,8 +103,9 @@ let of_value f = function
   let loc = match loc with
   | None -> []
   | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
-  let id = Stateid.to_xml id in
-  Element ("value", ["val", "fail"] @ loc, [id; Richpp.of_richpp msg])
+  let id = of_stateid id in
+  Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg])
+
 let to_value f = function
 | Element ("value", attrs, l) ->
   let ans = massoc "val" attrs in
@@ -106,8 +119,8 @@ let to_value f = function
       with Marshal_error | Failure _ -> None
     in
     let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise Marshal_error in
-    let id = Stateid.of_xml id in
-    let msg = Richpp.to_richpp msg in
+    let id = to_stateid id in
+    let msg = to_richpp msg in
     Fail (id, loc, msg)
   else raise Marshal_error
 | _ -> raise Marshal_error
@@ -134,14 +147,14 @@ let to_evar = function
   | _ -> raise Marshal_error
 
 let of_goal g =
-  let hyp = of_list Richpp.of_richpp g.goal_hyp in
-  let ccl = Richpp.of_richpp g.goal_ccl in
+  let hyp = of_list of_richpp g.goal_hyp in
+  let ccl = of_richpp g.goal_ccl in
   let id = of_string g.goal_id in
   Element ("goal", [], [id; hyp; ccl])
 let to_goal = function
   | Element ("goal", [], [id; hyp; ccl]) ->
-    let hyp = to_list Richpp.to_richpp hyp in
-    let ccl = Richpp.to_richpp ccl in
+    let hyp = to_list to_richpp hyp in
+    let ccl = to_richpp ccl in
     let id = to_string id in
     { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
   | _ -> raise Marshal_error
@@ -286,7 +299,7 @@ end = struct
       | Coq_object t  -> (of_coq_object (convert t))
       | Pair (t1,t2)  -> (of_pair (convert t1) (convert t2))
       | Union (t1,t2) -> (of_union (convert t1) (convert t2))
-      | State_id      -> Stateid.to_xml
+      | State_id      -> of_stateid
       | Search_cst    -> of_search_cst
     in
       convert ty
@@ -309,7 +322,7 @@ end = struct
       | Coq_object t  -> (to_coq_object (convert t))
       | Pair (t1,t2)  -> (to_pair (convert t1) (convert t2))
       | Union (t1,t2) -> (to_union (convert t1) (convert t2))
-      | State_id      -> Stateid.of_xml
+      | State_id      -> to_stateid
       | Search_cst    -> to_search_cst
     in
       convert ty
@@ -422,7 +435,7 @@ end = struct
       (pr_xml (of_bool true)) (pr_xml (of_bool false));
     Printf.printf "%s:\n\n%s\n\n" (print_val_t String) (pr_xml (of_string "hello"));
     Printf.printf "%s:\n\n%s\n\n" (print_val_t Int) (pr_xml (of_int 256));
-    Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (Stateid.to_xml Stateid.initial));
+    Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (of_stateid Stateid.initial));
     Printf.printf "%s:\n\n%s\n\n" (print_val_t (List Int)) (pr_xml (of_list of_int [3;4;5]));
     Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t (Option Int))
       (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None));
@@ -750,4 +763,128 @@ let document to_string_fmt =
       (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message"))));
   document_type_encoding to_string_fmt
 
+(* Moved from feedback.mli : This is IDE specific and we don't want to
+   pollute the core with it *)
+
+open Feedback
+
+let of_message_level = function
+  | Debug s ->
+      Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
+  | Info -> Serialize.constructor "message_level" "info" []
+  | Notice -> Serialize.constructor "message_level" "notice" []
+  | Warning -> Serialize.constructor "message_level" "warning" []
+  | Error -> Serialize.constructor "message_level" "error" []
+let to_message_level =
+  Serialize.do_match "message_level" (fun s args -> match s with
+  | "debug" -> Debug (Serialize.raw_string args)
+  | "info" -> Info
+  | "notice" -> Notice
+  | "warning" -> Warning
+  | "error" -> Error
+  | _ -> raise Serialize.Marshal_error)
+
+let of_message lvl msg =
+  let lvl     = of_message_level lvl in
+  let content = of_richpp msg        in
+  Xml_datatype.Element ("message", [], [lvl; content])
+
+let is_message = function
+  | Xml_datatype.Element ("message", [], [lvl; content]) ->
+    Some (to_message_level lvl, to_richpp content)
+  | _ -> None
+
+let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
+  | "addedaxiom", _ -> AddedAxiom
+  | "processed", _ -> Processed
+  | "processingin", [where] -> ProcessingIn (to_string where)
+  | "incomplete", _ -> Incomplete
+  | "complete", _ -> Complete
+  | "globref", [loc; filepath; modpath; ident; ty] ->
+       GlobRef(to_loc loc, to_string filepath,
+         to_string modpath, to_string ident, to_string ty)
+  | "globdef", [loc; ident; secpath; ty] ->
+       GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
+  | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
+  | "inprogress", [n] -> InProgress (to_int n)
+  | "workerstatus", [ns] ->
+       let n, s = to_pair to_string to_string ns in
+       WorkerStatus(n,s)
+  | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
+  (* | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) *)
+  | "filedependency", [from; dep] ->
+      FileDependency (to_option to_string from, to_string dep)
+  | "fileloaded", [dirpath; filename] ->
+      FileLoaded (to_string dirpath, to_string filename)
+  | "message", [lvl; content] ->
+     Message (to_message_level lvl, to_richpp content)
+
+  | _ -> raise Marshal_error)
+
+let of_feedback_content = function
+  | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
+  | Processed -> constructor "feedback_content" "processed" []
+  | ProcessingIn where ->
+      constructor "feedback_content" "processingin" [of_string where]
+  | Incomplete -> constructor "feedback_content" "incomplete" []
+  | Complete -> constructor "feedback_content" "complete" []
+  | GlobRef(loc, filepath, modpath, ident, ty) ->
+      constructor "feedback_content" "globref" [
+        of_loc loc;
+        of_string filepath;
+        of_string modpath;
+        of_string ident;
+        of_string ty ]
+  | GlobDef(loc, ident, secpath, ty) ->
+      constructor "feedback_content" "globdef" [
+        of_loc loc;
+        of_string ident;
+        of_string secpath;
+        of_string ty ]
+  | ErrorMsg(loc, s) ->
+      constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
+  | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
+  | WorkerStatus(n,s) ->
+      constructor "feedback_content" "workerstatus"
+        [of_pair of_string of_string (n,s)]
+  | Goals (loc,s) ->
+      constructor "feedback_content" "goals" [of_loc loc;of_string s]
+  (* | Custom (loc, name, x) -> *)
+  (*     constructor "feedback_content" "custom" [of_loc loc; of_string name; x] *)
+  | FileDependency (from, depends_on) ->
+      constructor "feedback_content" "filedependency" [
+        of_option of_string from;
+        of_string depends_on]
+  | FileLoaded (dirpath, filename) ->
+      constructor "feedback_content" "fileloaded" [
+        of_string dirpath;
+        of_string filename ]
+  | Message (l,m) -> constructor "feedback_content" "message" [ of_message l m ]
+
+let of_edit_or_state_id = function
+  | Edit id -> ["object","edit"], of_edit_id id
+  | State id -> ["object","state"], of_stateid id
+
+let of_feedback msg =
+  let content = of_feedback_content msg.contents in
+  let obj, id = of_edit_or_state_id msg.id in
+  let route = string_of_int msg.route in
+  Element ("feedback", obj @ ["route",route], [id;content])
+
+let to_feedback xml = match xml with
+  | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
+      id = Edit(to_edit_id id);
+      route = int_of_string route;
+      contents = to_feedback_content content }
+  | Element ("feedback", ["object","state";"route",route], [id;content]) -> { 
+      id = State(to_stateid id);
+      route = int_of_string route;
+      contents = to_feedback_content content }
+  | _ -> raise Marshal_error
+
+let is_feedback = function
+  | Element ("feedback", _, _) -> true
+  | _ -> false
+
 (* vim: set foldmethod=marker: *)
+
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 265a50c47..6bca8772e 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 *)
+
diff --git a/lib/feedback.ml b/lib/feedback.ml
index dce4372ec..d6f580fd1 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Xml_datatype
-open Serialize
 
 type level =
   | Debug of string
@@ -16,42 +15,6 @@ type level =
   | Warning
   | Error
 
-type message = {
-  message_level : level;
-  message_content : xml;
-}
-
-let of_message_level = function
-  | Debug s ->
-      Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
-  | Info -> Serialize.constructor "message_level" "info" []
-  | Notice -> Serialize.constructor "message_level" "notice" []
-  | Warning -> Serialize.constructor "message_level" "warning" []
-  | Error -> Serialize.constructor "message_level" "error" []
-let to_message_level =
-  Serialize.do_match "message_level" (fun s args -> match s with
-  | "debug" -> Debug (Serialize.raw_string args)
-  | "info" -> Info
-  | "notice" -> Notice
-  | "warning" -> Warning
-  | "error" -> Error
-  | _ -> raise Serialize.Marshal_error)
-
-let of_message msg =
-  let lvl = of_message_level msg.message_level in
-  let content = Serialize.of_xml msg.message_content in
-  Xml_datatype.Element ("message", [], [lvl; content])
-let to_message xml = match xml with
-  | Xml_datatype.Element ("message", [], [lvl; content]) -> {
-      message_level = to_message_level lvl;
-      message_content = Serialize.to_xml content }
-  | _ -> raise Serialize.Marshal_error
-
-let is_message = function
-  | Xml_datatype.Element ("message", _, _) -> true
-  | _ -> false
-
-
 type edit_id = int
 type state_id = Stateid.t
 type edit_or_state_id = Edit of edit_id | State of state_id
@@ -71,8 +34,10 @@ type feedback_content =
   | GlobDef of Loc.t * string * string * string
   | FileDependency of string option * string
   | FileLoaded of string * string
+  (* Extra metadata *)
   | Custom of Loc.t * string * xml
-  | Message of message
+  (* Old generic messages *)
+  | Message of level * Richpp.richpp
 
 type feedback = {
   id : edit_or_state_id;
@@ -80,94 +45,6 @@ type feedback = {
   route : route_id;
 }
 
-let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
-  | "addedaxiom", _ -> AddedAxiom
-  | "processed", _ -> Processed
-  | "processingin", [where] -> ProcessingIn (to_string where)
-  | "incomplete", _ -> Incomplete
-  | "complete", _ -> Complete
-  | "globref", [loc; filepath; modpath; ident; ty] ->
-       GlobRef(to_loc loc, to_string filepath,
-         to_string modpath, to_string ident, to_string ty)
-  | "globdef", [loc; ident; secpath; ty] ->
-       GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
-  | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
-  | "inprogress", [n] -> InProgress (to_int n)
-  | "workerstatus", [ns] ->
-       let n, s = to_pair to_string to_string ns in
-       WorkerStatus(n,s)
-  | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
-  | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
-  | "filedependency", [from; dep] ->
-      FileDependency (to_option to_string from, to_string dep)
-  | "fileloaded", [dirpath; filename] ->
-      FileLoaded (to_string dirpath, to_string filename)
-  | "message", [m] -> Message (to_message m)
-  | _ -> raise Marshal_error)
-let of_feedback_content = function
-  | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
-  | Processed -> constructor "feedback_content" "processed" []
-  | ProcessingIn where ->
-      constructor "feedback_content" "processingin" [of_string where]
-  | Incomplete -> constructor "feedback_content" "incomplete" []
-  | Complete -> constructor "feedback_content" "complete" []
-  | GlobRef(loc, filepath, modpath, ident, ty) ->
-      constructor "feedback_content" "globref" [
-        of_loc loc;
-        of_string filepath;
-        of_string modpath;
-        of_string ident;
-        of_string ty ]
-  | GlobDef(loc, ident, secpath, ty) ->
-      constructor "feedback_content" "globdef" [
-        of_loc loc;
-        of_string ident;
-        of_string secpath;
-        of_string ty ]
-  | ErrorMsg(loc, s) ->
-      constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
-  | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
-  | WorkerStatus(n,s) ->
-      constructor "feedback_content" "workerstatus"
-        [of_pair of_string of_string (n,s)]
-  | Goals (loc,s) ->
-      constructor "feedback_content" "goals" [of_loc loc;of_string s]
-  | Custom (loc, name, x) ->
-      constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
-  | FileDependency (from, depends_on) ->
-      constructor "feedback_content" "filedependency" [
-        of_option of_string from;
-        of_string depends_on]
-  | FileLoaded (dirpath, filename) ->
-      constructor "feedback_content" "fileloaded" [
-        of_string dirpath;
-        of_string filename ]
-  | Message m -> constructor "feedback_content" "message" [ of_message m ]
-
-let of_edit_or_state_id = function
-  | Edit id -> ["object","edit"], of_edit_id id
-  | State id -> ["object","state"], Stateid.to_xml id
-
-let of_feedback msg =
-  let content = of_feedback_content msg.contents in
-  let obj, id = of_edit_or_state_id msg.id in
-  let route = string_of_int msg.route in
-  Element ("feedback", obj @ ["route",route], [id;content])
-let to_feedback xml = match xml with
-  | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
-      id = Edit(to_edit_id id);
-      route = int_of_string route;
-      contents = to_feedback_content content }
-  | Element ("feedback", ["object","state";"route",route], [id;content]) -> { 
-      id = State(Stateid.of_xml id);
-      route = int_of_string route;
-      contents = to_feedback_content content }
-  | _ -> raise Marshal_error
-
-let is_feedback = function
-  | Element ("feedback", _, _) -> true
-  | _ -> false
-
 let default_route = 0
 
 (** Feedback and logging *)
@@ -264,11 +141,8 @@ let feedback ?id ?route what =
   }
 
 let feedback_logger lvl msg =
-  feedback ~route:!feedback_route ~id:!feedback_id (
-    Message {
-      message_level   = lvl;
-      message_content = Richpp.of_richpp (Richpp.richpp_of_pp msg);
-    })
+  feedback ~route:!feedback_route ~id:!feedback_id
+    (Message (lvl, Richpp.richpp_of_pp msg))
 
 (* Output to file *)
 let ft_logger old_logger ft level mesg =
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 *)
diff --git a/lib/richpp.ml b/lib/richpp.ml
index fe3edd99c..a98273edb 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -194,7 +194,3 @@ let raw_print xml =
   let () = print xml in
   Buffer.contents buf
 
-let of_richpp x = Element ("richpp", [], [x])
-let to_richpp xml = match xml with
-| Element ("richpp", [], [x]) -> x
-| _ -> raise Serialize.Marshal_error
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 807d52aba..287d265a8 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -57,10 +57,7 @@ val richpp_of_string : string -> richpp
 val repr : richpp -> Xml_datatype.xml
 (** Observe the styled text as XML *)
 
-(** {5 Serialization} *)
-
-val of_richpp : richpp -> Xml_datatype.xml
-val to_richpp : Xml_datatype.xml -> richpp
+(** {5 Debug/Compat} *)
 
 (** Represent the semi-structured document as a string, dropping any additional
     information. *)
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 59cf206e2..c17df2b32 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Xml_datatype
-
 type t = int
 let initial = 1
 let dummy = 0
@@ -15,20 +13,14 @@ let fresh, in_range =
   let cur = ref initial in
   (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
 let to_string = string_of_int
-let of_int id = assert(in_range id); id
+let of_int id =
+  (* Coqide too to parse ids too, but cannot check if they are valid.
+   * Hence we check for validity only if we are an ide slave. *)
+  if !Flags.ide_slave then assert (in_range id);
+  id
 let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
-let of_xml = function
-  | Element ("state_id",["val",i],[]) ->
-      let id = int_of_string i in
-      (* Coqide too to parse ids too, but cannot check if they are valid.
-       * Hence we check for validity only if we are an ide slave. *)
-      if !Flags.ide_slave then assert(in_range id);
-      id
-  | _ -> raise (Invalid_argument "to_state_id")
-let to_xml i = Element ("state_id",["val",string_of_int i],[])
-
 let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
 let add exn ?(valid = initial) id =
   Exninfo.add exn state_id_info (valid, id)
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 2c12c30c3..516ad891f 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Xml_datatype
-
 type t
 
 val equal : t -> t -> bool
@@ -19,13 +17,11 @@ val initial : t
 val dummy : t
 val fresh : unit -> t
 val to_string : t -> string
+
 val of_int : int -> t
 val to_int : t -> int
-val newer_than : t -> t -> bool
 
-(* XML marshalling *)
-val to_xml : t -> xml
-val of_xml : xml -> t
+val newer_than : t -> t -> bool
 
 (* Attaches to an exception the concerned state id, plus an optional
  * state id that is a valid state id before the error.
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);