Move XML serialization to ide/ folder.

32 files changed, 246 insertions, 239 deletions

diff --git a/.gitignore b/.gitignore
index 4f8c019f46..06cac2fee6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -112,7 +112,7 @@ tools/coqwc.ml
 tools/coqdep_lexer.ml
 tools/ocamllibdep.ml
 tools/coqdoc/cpretty.ml
-lib/xml_lexer.ml
+ide/xml_lexer.ml
 
 # .ml4 files
 
diff --git a/Makefile.build b/Makefile.build
index 10926daa1c..4fac65df75 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -729,7 +729,12 @@ $(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
+$(FAKEIDE): lib/clib$(BESTLIB) lib/errors$(BESTOBJ)			\
+	    lib/spawn$(BESTOBJ) ide/document$(BESTOBJ)			\
+	    ide/serialize$(BESTOBJ) ide/xml_lexer$(BESTOBJ)		\
+	    ide/xml_parser$(BESTOBJ) ide/xml_printer$(BESTOBJ)		\
+	    ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) |	\
+	    $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,-I ide,str unix threads)
 
diff --git a/ide/coq.ml b/ide/coq.ml
index 7a32faffca..82fd48c9e0 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/coqidetop.mllib b/ide/coqidetop.mllib
index 92301dc30e..ed1fa465d2 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -1,2 +1,9 @@
+Xml_lexer
+Xml_parser
+Xml_printer
+Serialize
+Richprinter
 Xmlprotocol
+Texmacspp
+Document
 Ide_slave
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 83b3142839..b2f32fcf7b 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -14,8 +14,13 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Ideutils
+Serialize
+Richprinter
+Xml_lexer
+Xml_parser
+Xml_printer
 Xmlprotocol
+Ideutils
 Coq
 Coq_lex
 Sentence
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 59efc2d821..0e09d84095 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -393,6 +393,15 @@ let interp ((_raw, verbose), s) =
 
 let quit = ref false
 
+(** Serializes the output of Stm.get_ast  *)
+let print_ast id =
+  match Stm.get_ast id with
+  | Some (expr, loc) -> begin
+      try  Texmacspp.tmpp expr loc
+      with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
+    end
+  | None     -> Xml_datatype.PCData "ERROR"
+
 (** Grouping all call handlers together + error handling *)
 
 let eval_call xml_oc log c =
@@ -423,7 +432,7 @@ let eval_call xml_oc log c =
     Interface.interp = interruptible interp;
     Interface.handle_exn = handle_exn;
     Interface.stop_worker = Stm.stop_worker;
-    Interface.print_ast = Stm.print_ast;
+    Interface.print_ast = print_ast;
     Interface.annotate = interruptible annotate;
   } in
   Xmlprotocol.abstract_eval_call handler c
@@ -444,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/printing/richprinter.ml b/ide/richprinter.ml
index 5f39f36eab..5f39f36eab 100644
--- a/printing/richprinter.ml
+++ b/ide/richprinter.ml
diff --git a/printing/richprinter.mli b/ide/richprinter.mli
index c9e84e3eb4..c9e84e3eb4 100644
--- a/printing/richprinter.mli
+++ b/ide/richprinter.mli
diff --git a/lib/serialize.ml b/ide/serialize.ml
index 685ec6049c..685ec6049c 100644
--- a/lib/serialize.ml
+++ b/ide/serialize.ml
diff --git a/lib/serialize.mli b/ide/serialize.mli
index d7c14e7e73..d7c14e7e73 100644
--- a/lib/serialize.mli
+++ b/ide/serialize.mli
diff --git a/stm/texmacspp.ml b/ide/texmacspp.ml
index d1d6de9ae8..d1d6de9ae8 100644
--- a/stm/texmacspp.ml
+++ b/ide/texmacspp.ml
diff --git a/stm/texmacspp.mli b/ide/texmacspp.mli
index 858847fb6a..858847fb6a 100644
--- a/stm/texmacspp.mli
+++ b/ide/texmacspp.mli
diff --git a/lib/xml_lexer.mli b/ide/xml_lexer.mli
index e61cb055f7..e61cb055f7 100644
--- a/lib/xml_lexer.mli
+++ b/ide/xml_lexer.mli
diff --git a/lib/xml_lexer.mll b/ide/xml_lexer.mll
index 290f2c89ab..290f2c89ab 100644
--- a/lib/xml_lexer.mll
+++ b/ide/xml_lexer.mll
diff --git a/lib/xml_parser.ml b/ide/xml_parser.ml
index 8db3f9e8ba..8db3f9e8ba 100644
--- a/lib/xml_parser.ml
+++ b/ide/xml_parser.ml
diff --git a/lib/xml_parser.mli b/ide/xml_parser.mli
index ac2eab352f..ac2eab352f 100644
--- a/lib/xml_parser.mli
+++ b/ide/xml_parser.mli
diff --git a/lib/xml_printer.ml b/ide/xml_printer.ml
index e7e4d0cebc..e7e4d0cebc 100644
--- a/lib/xml_printer.ml
+++ b/ide/xml_printer.ml
diff --git a/lib/xml_printer.mli b/ide/xml_printer.mli
index f24f51fff5..f24f51fff5 100644
--- a/lib/xml_printer.mli
+++ b/ide/xml_printer.mli
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 232630e5b2..45279a7c3f 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 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 *)
+
diff --git a/lib/clib.mllib b/lib/clib.mllib
index c3ec4a696e..95007c52ab 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -21,7 +21,6 @@ Control
 Loc
 CList
 CString
-Serialize
 Deque
 CObj
 CArray
@@ -33,9 +32,6 @@ Ppstyle
 Xml_datatype
 Richpp
 Feedback
-Xml_lexer
-Xml_parser
-Xml_printer
 CUnix
 Envars
 Aux_file
diff --git a/lib/feedback.ml b/lib/feedback.ml
index dce4372ec0..d6f580fd16 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 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 *)
diff --git a/lib/richpp.ml b/lib/richpp.ml
index fe3edd99ca..a98273edb2 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 807d52aba4..287d265a8f 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 59cf206e2e..c17df2b321 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 2c12c30c3c..516ad891ff 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/printing/printing.mllib b/printing/printing.mllib
index 652a34fa1f..52102e1d3b 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -10,4 +10,3 @@ Printmod
 Prettyp
 Ppvernac
 Ppvernacsig
-Richprinter
diff --git a/stm/stm.ml b/stm/stm.ml
index 28e749d5c8..e2acb10293 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2314,18 +2314,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
     let e = Errors.push e in
     handle_failure e vcs tty
 
-let print_ast id =
-  try
-    match VCS.visit id with
-    | { step = `Cmd { cast = { loc; expr } } }
-    | { step = `Fork (({ loc; expr }, _, _, _), _) } 
-    | { step = `Qed ({ qast = { loc; expr } }, _) } ->
-        let xml = 
-          try Texmacspp.tmpp expr loc
-          with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in
-        xml;
-    | _ -> Xml_datatype.PCData "ERROR"
-  with _ -> Xml_datatype.PCData "ERROR"
+let get_ast id =
+  match VCS.visit id with
+  | { step = `Cmd { cast = { loc; expr } } }
+  | { step = `Fork (({ loc; expr }, _, _, _), _) } 
+  | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+         Some (expr, loc)
+  | _ -> None
 
 let stop_worker n = Slaves.cancel_worker n
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 6519a62541..6ffe0beb44 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -76,7 +76,9 @@ val get_current_state : unit -> Stateid.t
 
 (* Misc *)
 val init : unit -> unit
-val print_ast : Stateid.t -> Xml_datatype.xml
+
+(* This returns the node at that position *)
+val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
 
 (* Filename *)
 val set_compilation_hints : string -> unit
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 92b3a869a9..bd792b01f6 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,5 @@ Vernac_classifier
 Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
-Texmacspp
 Stm
 Vio_checking
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d5ef807b68..221fb36d8d 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);