all coqide specific files moved into ide/

lib/interface split into:
 - lib/feedback
     subscribe-based feedback bus (also used by coqidetop)
 - ide/interface
     definition of coqide protocol messages
   lib/pp
     structured info/err/warn messages

lib/serialize split into:
 - lib/serialize
     generic xml serialization (list, pairs, int, loc, ...)
     used by coqide but potentially useful to other interfaces
 - ide/xmlprotocol
     serialization of protocol messages as in ide/interface

the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/

41 files changed, 1199 insertions, 1045 deletions

diff --git a/Makefile.build b/Makefile.build
index 0f05dc606..6bd638656 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -293,7 +293,7 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
 # target to build CoqIde
 coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
 
-COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) -thread
 
 .SUFFIXES:.vo
 
@@ -536,7 +536,7 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ)))
 # 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) tools/fake_ide$(BESTOBJ)
+$(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)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,-I ide,str unix)
 
diff --git a/Makefile.common b/Makefile.common
index 4b6cc764a..8a70273ad 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -72,11 +72,10 @@ PLUGINS:=\
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \
-  tools 	tools/coqdoc	idetop\
+  tools 	tools/coqdoc	\
   $(addprefix plugins/, $(PLUGINS))
 
-IDESRCDIRS:=\
-  config	lib	ide/utils	ide
+IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
 
 # Order is relevent here because kernel and checker contain files
 # with the same name
@@ -214,7 +213,7 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
 IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo
 IDECMA:=ide/ide.cma
-IDETOPLOOPCMA=idetop/coqidetop.cma
+IDETOPLOOPCMA=ide/coqidetop.cma
 
 LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml
 LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
@@ -227,7 +226,7 @@ IDEMOD:=$(shell cat ide/ide.mllib)
 
 # coqmktop, coqc
 
-COQENVCMO:=lib/clib.cma lib/loc.cmo lib/errors.cmo
+COQENVCMO:=lib/clib.cma lib/errors.cmo
 
 COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 766eb4182..cbabd208c 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -15,8 +15,9 @@ Backtrace
 Flags
 Control
 Pp_control
-Pp
 Loc
+Serialize
+Pp
 Segmenttree
 Unicodetable
 Unicode
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 81fcc8493..dcd3f0efb 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -18,6 +18,8 @@ Loc
 Compat
 Flags
 Control
+Loc
+Serialize
 Pp
 Segmenttree
 Unicodetable
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 338d44fbf..a18951f4b 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -14,8 +14,9 @@ Exninfo
 Backtrace
 Pp_control
 Flags
-Pp
 Loc
+Serialize
+Pp
 Errors
 CList
 CString
diff --git a/ide/coq.ml b/ide/coq.ml
index af00cc63c..c1555e57f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -177,7 +177,7 @@ type void = Void
     Reference: http://alan.petitepomme.net/cwn/2004.01.13.html
     To rewrite someday with GADT. *)
 
-type 'a poly_ccb = 'a Serialize.call * ('a Interface.value -> void)
+type 'a poly_ccb = 'a Xmlprotocol.call * ('a Interface.value -> void)
 type 't scoped_ccb = { bind_ccb : 'a. 'a poly_ccb -> 't }
 type ccb = { open_ccb : 't. 't scoped_ccb -> 't }
 
@@ -234,7 +234,7 @@ type coqtop = {
   (* called whenever coqtop dies *)
   mutable reset_handler : reset_kind -> unit task;
   (* called whenever coqtop sends a feedback message *)
-  mutable feedback_handler : Interface.feedback -> unit;
+  mutable feedback_handler : Feedback.feedback -> unit;
   (* actual coqtop process and its status *)
   mutable handle : handle;
   mutable status : status;
@@ -296,22 +296,22 @@ let rec check_errors = function
 | `OUT :: _ -> raise (TubeError "OUT")
 
 let handle_intermediate_message handle xml =
-  let message = Serialize.to_message xml in
-  let level = message.Interface.message_level in
-  let content = message.Interface.message_content in
+  let message = Pp.to_message xml in
+  let level = message.Pp.message_level in
+  let content = message.Pp.message_content in
   let logger = match handle.waiting_for with
     | Some (_, l) -> l 
     | None -> function
-        | Interface.Error -> Minilib.log ~level:`ERROR
-        | Interface.Info -> Minilib.log ~level:`INFO
-        | Interface.Notice -> Minilib.log ~level:`NOTICE
-        | Interface.Warning -> Minilib.log ~level:`WARNING
-        | Interface.Debug _ -> Minilib.log ~level:`DEBUG
+        | Pp.Error -> Minilib.log ~level:`ERROR
+        | Pp.Info -> Minilib.log ~level:`INFO
+        | Pp.Notice -> Minilib.log ~level:`NOTICE
+        | Pp.Warning -> Minilib.log ~level:`WARNING
+        | Pp.Debug _ -> Minilib.log ~level:`DEBUG
   in
   logger level content
 
 let handle_feedback feedback_processor xml =
-  let feedback = Serialize.to_feedback xml in
+  let feedback = Feedback.to_feedback xml in
   feedback_processor feedback
 
 let handle_final_answer handle xml =
@@ -320,7 +320,7 @@ let handle_final_answer handle xml =
     | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml))
     | Some (c, _) -> c in
   let () = handle.waiting_for <- None in
-  with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer c xml) }
+  with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) }
 
 type input_state = {
   mutable fragment : string;
@@ -340,10 +340,10 @@ 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 Serialize.is_message xml then begin
+    if Pp.is_message xml then begin
       handle_intermediate_message handle xml;
       loop ()
-    end else if Serialize.is_feedback xml then begin
+    end else if Feedback.is_feedback xml then begin
       handle_feedback feedback_processor xml;
       loop ()
     end else begin
@@ -501,22 +501,22 @@ type 'a query = 'a Interface.value task
 
 let eval_call ?(logger=default_logger) call handle k =
   (** Send messages to coqtop and prepare the decoding of the answer *)
-  Minilib.log ("Start eval_call " ^ Serialize.pr_call call);
+  Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call);
   assert (handle.alive && handle.waiting_for = None);
   handle.waiting_for <- Some (mk_ccb (call,k), logger);
-  Xml_printer.print handle.xml_oc (Serialize.of_call call);
+  Xml_printer.print handle.xml_oc (Xmlprotocol.of_call call);
   Minilib.log "End eval_call";
   Void
 
-let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x)
-let edit_at i = eval_call (Serialize.edit_at i)
-let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x)
-let mkcases s = eval_call (Serialize.mkcases s)
-let status ?logger force = eval_call ?logger (Serialize.status force)
-let hints x = eval_call (Serialize.hints x)
-let search flags = eval_call (Serialize.search flags)
-let init x = eval_call (Serialize.init x)
-let stop_worker x = eval_call (Serialize.stop_worker x)
+let add ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.add x)
+let edit_at i = eval_call (Xmlprotocol.edit_at i)
+let query ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.query x)
+let mkcases s = eval_call (Xmlprotocol.mkcases s)
+let status ?logger force = eval_call ?logger (Xmlprotocol.status force)
+let hints x = eval_call (Xmlprotocol.hints x)
+let search flags = eval_call (Xmlprotocol.search flags)
+let init x = eval_call (Xmlprotocol.init x)
+let stop_worker x = eval_call (Xmlprotocol.stop_worker x)
 
 module PrintOpt =
 struct
@@ -573,7 +573,7 @@ struct
     let mkopt o v acc = (o, Interface.BoolValue v) :: acc in
     let opts = Hashtbl.fold mkopt current_state [] in
     let opts = (width, Interface.IntValue !width_state) :: opts in
-    eval_call (Serialize.set_options opts) h
+    eval_call (Xmlprotocol.set_options opts) h
       (function
 	| Interface.Good () -> k ()
 	| _ -> failwith "Cannot set options. Resetting coqtop")
@@ -581,7 +581,7 @@ struct
 end
 
 let goals ?logger x h k =
-  PrintOpt.enforce h (fun () -> eval_call ?logger (Serialize.goals x) h k)
+  PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k)
 
 let evars x h k =
-  PrintOpt.enforce h (fun () -> eval_call (Serialize.evars x) h k)
+  PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.evars x) h k)
diff --git a/ide/coq.mli b/ide/coq.mli
index 542cc4462..966c77700 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -63,7 +63,7 @@ val spawn_coqtop : string list -> coqtop
 val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
 (** Register a handler called when a coqtop dies (badly or on purpose) *)
 
-val set_feedback_handler : coqtop -> (Interface.feedback -> unit) -> unit
+val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit
 (** Register a handler called when coqtop sends a feedback message *)
 
 val init_coqtop : coqtop -> unit task -> unit
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index ab1a86f78..cefe18092 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -10,6 +10,7 @@ open Util
 open Coq
 open Ideutils
 open Interface
+open Feedback
 
 type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string ]
 type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ]
@@ -422,7 +423,7 @@ object(self)
       self#position_error_tag_at_iter start phrase loc;
       buffer#place_cursor ~where:stop;
       messages#clear;
-      messages#push Error msg;
+      messages#push Pp.Error msg;
       self#show_goals
     end else
       self#show_goals_aux ~move_insert:true ()
@@ -511,7 +512,7 @@ object(self)
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Notice msg;
+                  logger Pp.Notice msg;
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -519,7 +520,7 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Notice msg;
+                  logger Pp.Notice msg;
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
@@ -538,7 +539,7 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Info "Doc checked";
+         messages#push Pp.Info "Doc checked";
          Coq.return ()
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status ~logger:messages#push true) next
@@ -628,8 +629,8 @@ object(self)
           self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
-          if loc <> None then messages#push Error "Fixme LOC";
-          messages#push Error msg;
+          if loc <> None then messages#push Pp.Error "Fixme LOC";
+          messages#push Pp.Error msg;
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
           else undo safe_id
                  (Doc.focused document && Doc.is_in_focus document safe_id))
@@ -647,7 +648,7 @@ object(self)
     ?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
   =
     messages#clear;
-    messages#push Error msg;
+    messages#push Pp.Error msg;
     ignore(self#process_feedback ());
     if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
     else
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e20c95b9e..9614c6f3b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -739,7 +739,7 @@ let coqtop_arguments sn =
         let args = String.concat " " args in
         let msg = Printf.sprintf "Invalid arguments: %s" args in
         let () = sn.messages#clear in
-        sn.messages#push Interface.Error msg
+        sn.messages#push Pp.Error msg
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ok_cb in
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
new file mode 100644
index 000000000..92301dc30
--- /dev/null
+++ b/ide/coqidetop.mllib
@@ -0,0 +1,2 @@
+Xmlprotocol
+Ide_slave
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 8bc1337ff..944476171 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -15,6 +15,7 @@ Utf8_convert
 Preferences
 Project_file
 Ideutils
+Xmlprotocol
 Coq
 Coq_lex
 Sentence
diff --git a/idetop/ide_slave.ml b/ide/ide_slave.ml
index 2185084a0..6b2c52123 100644
--- a/idetop/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -50,9 +50,9 @@ let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 let pr_debug s =
   if !Flags.debug then pr_with_pid s
 let pr_debug_call q =
-  if !Flags.debug then pr_with_pid ("<-- " ^ Serialize.pr_call q)
+  if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
 let pr_debug_answer q r =
-  if !Flags.debug then pr_with_pid ("--> " ^ Serialize.pr_full_value q r)
+  if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)
 
 (** Categories of commands *)
 
@@ -277,7 +277,7 @@ let set_options options =
 
 let about () = {
   Interface.coqtop_version = Coq_config.version;
-  Interface.protocol_version = Serialize.protocol_version;
+  Interface.protocol_version = Xmlprotocol.protocol_version;
   Interface.release_date = Coq_config.date;
   Interface.compile_date = Coq_config.compile_date;
 }
@@ -365,7 +365,7 @@ let eval_call xml_oc log c =
     Interface.handle_exn = handle_exn;
     Interface.stop_worker = Stm.stop_worker;
   } in
-  Serialize.abstract_eval_call handler c
+  Xmlprotocol.abstract_eval_call handler c
 
 (** Message dispatching.
     Since coqtop -ideslave starts 1 thread per slave, and each
@@ -384,15 +384,15 @@ let slave_logger xml_oc level message =
   (* convert the message into XML *)
   let msg = string_of_ppcmds (hov 0 message) in
   let message = {
-    Interface.message_level = level;
-    Interface.message_content = msg;
+    Pp.message_level = level;
+    Pp.message_content = msg;
   } in
   let () = pr_debug (Printf.sprintf "-> %S" msg) in
-  let xml = Serialize.of_message message in
+  let xml = Pp.of_message message in
   print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
-  let xml = Serialize.of_feedback msg in
+  let xml = Feedback.of_feedback msg in
   print_xml xml_oc xml
 
 (** The main loop *)
@@ -421,12 +421,12 @@ let loop () =
     try
       let xml_query = Xml_parser.parse xml_ic in
 (*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
-      let q = Serialize.to_call xml_query in
+      let q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
-      let r = eval_call xml_oc (slave_logger xml_oc Interface.Notice) q in
+      let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) q in
       let () = pr_debug_answer q r in
-(*       pr_with_pid (Xml_printer.to_string_fmt (Serialize.of_answer q r)); *)
-      print_xml xml_oc (Serialize.of_answer q r);
+(*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
+      print_xml xml_oc (Xmlprotocol.of_answer q r);
       flush out_ch
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->
@@ -445,7 +445,14 @@ let loop () =
   pr_debug "Exiting gracefully.";
   exit 0
 
+let rec parse = function
+  | "--help-XML-protocol" :: rest ->
+        Xmlprotocol.document Xml_printer.to_string_fmt; exit 0
+  | x :: rest -> x :: parse rest
+  | [] -> []
+
 let () = Coqtop.toploop_init := (fun args ->
+        let args = parse args in
         Flags.make_silent true;
         init_stdout ();
         args)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d8ca34f98..32d2bb97b 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -272,15 +272,15 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Interface.message_level -> string -> unit
+type logger = Pp.message_level -> string -> unit
 
 let default_logger level message =
   let level = match level with
-  | Interface.Debug _ -> `DEBUG
-  | Interface.Info -> `INFO
-  | Interface.Notice -> `NOTICE
-  | Interface.Warning -> `WARNING
-  | Interface.Error -> `ERROR
+  | Pp.Debug _ -> `DEBUG
+  | Pp.Info -> `INFO
+  | Pp.Notice -> `NOTICE
+  | Pp.Warning -> `WARNING
+  | Pp.Error -> `ERROR
   in
   Minilib.log ~level message
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 5fd97e3a5..5877d1270 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -69,9 +69,9 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Interface.message_level -> string -> unit
+type logger = Pp.message_level -> string -> unit
 
-val default_logger : Interface.message_level -> string -> unit
+val default_logger : Pp.message_level -> string -> unit
 (** Default logger. It logs messages that the casual user should not see. *)
 
 (** {6 I/O operations} *)
diff --git a/lib/interface.mli b/ide/interface.mli
index c8fe068e6..4e5e4a9cd 100644
--- a/lib/interface.mli
+++ b/ide/interface.mli
@@ -55,13 +55,13 @@ type hint = (string * string) list
 
 type option_name = string list
 
-type option_value =
+type option_value = Goptions.option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
 
 (** Summary of an option status *)
-type option_state = {
+type option_state = Goptions.option_state = {
   opt_sync  : bool;
   (** Whether an option is synchronous *)
   opt_depr  : bool;
@@ -72,7 +72,7 @@ type option_state = {
   (** The current value of the option *)
 }
 
-type search_constraint =
+type search_constraint = Search.search_constraint =
 (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
 | Name_Pattern of string
 (** Whether the object type satisfies a pattern *)
@@ -92,7 +92,7 @@ type search_flags = (search_constraint * bool) list
     the user. [coq_object_prefix] is the missing part to recover the fully
     qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
     [coq_object_object] is the actual content of the object. *)
-type 'a coq_object = {
+type 'a coq_object = 'a Search.coq_object = {
   coq_object_prefix : string list;
   coq_object_qualid : string list;
   coq_object_object : 'a;
@@ -105,45 +105,11 @@ type coq_info = {
   compile_date : string;
 }
 
-(** Coq unstructured messages *)
-
-type message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = {
-  message_level : message_level;
-  message_content : string;
-}
-
-(** 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 feedback_content =
-  | AddedAxiom
-  | Processed
-  | Incomplete
-  | Complete
-  | GlobRef of Loc.t * string * string * string * string
-  | GlobDef of Loc.t * string * string * string
-  | ErrorMsg of Loc.t * string
-  | InProgress of int
-  | SlaveStatus of int * string
-  | ProcessingInMaster
-
-type feedback = {
-  id : edit_or_state_id;
-  content : feedback_content;
-}
-
 (** Calls result *)
 
 type location = (int * int) option (* start and end of the error *)
+type state_id = Feedback.state_id
+type edit_id = Feedback.edit_id
 
 (* The fail case carries the current state_id of the prover, the GUI
    should probably retract to that point *)
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index f58cdc647..cd3e31135 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -12,7 +12,7 @@ class type message_view =
     method clear : unit
     method add : string -> unit
     method set : string -> unit
-    method push : Interface.message_level -> string -> unit
+    method push : Pp.message_level -> string -> unit
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
       (** for more advanced text edition *)
@@ -43,8 +43,8 @@ let message_view () : message_view =
 
     method push level msg =
       let tags = match level with
-      | Interface.Error -> [Tags.Message.error]
-      | Interface.Warning -> [Tags.Message.warning]
+      | Pp.Error -> [Tags.Message.error]
+      | Pp.Warning -> [Tags.Message.warning]
       | _ -> []
       in
       if msg <> "" then begin
@@ -52,7 +52,7 @@ let message_view () : message_view =
         buffer#insert ~tags "\n"
       end
 
-    method add msg = self#push Interface.Notice msg
+    method add msg = self#push Pp.Notice msg
 
     method set msg = self#clear; self#add msg
 
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index cb84ae733..8a0a2bd85 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -12,7 +12,7 @@ class type message_view =
     method clear : unit
     method add : string -> unit
     method set : string -> unit
-    method push : Interface.message_level -> string -> unit
+    method push : Pp.message_level -> string -> unit
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
       (** for more advanced text edition *)
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
new file mode 100644
index 000000000..09626172d
--- /dev/null
+++ b/ide/xmlprotocol.ml
@@ -0,0 +1,701 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Protocol version of this file. This is the date of the last modification. *)
+
+(** WARNING: TO BE UPDATED WHEN MODIFIED! *)
+
+let protocol_version = "20140312"
+
+(** * Interface of calls to Coq by CoqIde *)
+
+open Util
+open Interface
+open Serialize
+open Xml_datatype
+
+(* Marshalling of basic types and type constructors *)
+module Xml_marshalling = struct
+
+let of_search_cst = function
+  | Name_Pattern s ->
+    constructor "search_cst" "name_pattern" [of_string s]
+  | Type_Pattern s ->
+    constructor "search_cst" "type_pattern" [of_string s]
+  | SubType_Pattern s ->
+    constructor "search_cst" "subtype_pattern" [of_string s]
+  | In_Module m ->
+    constructor "search_cst" "in_module" [of_list of_string m]
+  | Include_Blacklist ->
+    constructor "search_cst" "include_blacklist" []
+let to_search_cst = do_match "search_cst" (fun s args -> match s with
+  | "name_pattern" -> Name_Pattern (to_string (singleton args))
+  | "type_pattern" -> Type_Pattern (to_string (singleton args))
+  | "subtype_pattern" -> SubType_Pattern (to_string (singleton args))
+  | "in_module" -> In_Module (to_list to_string (singleton args))
+  | "include_blacklist" -> Include_Blacklist
+  | _ -> raise Marshal_error)
+
+let of_coq_object f ans =
+  let prefix = of_list of_string ans.coq_object_prefix in
+  let qualid = of_list of_string ans.coq_object_qualid in
+  let obj = f ans.coq_object_object in
+  Element ("coq_object", [], [prefix; qualid; obj])
+
+let to_coq_object f = function
+| Element ("coq_object", [], [prefix; qualid; obj]) ->
+  let prefix = to_list to_string prefix in
+  let qualid = to_list to_string qualid in
+  let obj = f obj in {
+    coq_object_prefix = prefix;
+    coq_object_qualid = qualid;
+    coq_object_object = obj;
+  }
+| _ -> raise Marshal_error
+
+let of_option_value = function
+  | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i]
+  | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b]
+  | StringValue s -> constructor "option_value" "stringvalue" [of_string s]
+let to_option_value = do_match "option_value" (fun s args -> match s with
+  | "intvalue" -> IntValue (to_option to_int (singleton args))
+  | "boolvalue" -> BoolValue (to_bool (singleton args))
+  | "stringvalue" -> StringValue (to_string (singleton args))
+  | _ -> raise Marshal_error)
+
+let of_option_state s =
+  Element ("option_state", [], [
+    of_bool s.opt_sync;
+    of_bool s.opt_depr;
+    of_string s.opt_name;
+    of_option_value s.opt_value])
+let to_option_state = function
+  | Element ("option_state", [], [sync; depr; name; value]) -> {
+      opt_sync = to_bool sync;
+      opt_depr = to_bool depr;
+      opt_name = to_string name;
+      opt_value = to_option_value value }
+  | _ -> raise Marshal_error
+
+
+let of_value f = function
+| Good x -> Element ("value", ["val", "good"], [f x])
+| Fail (id,loc, msg) ->
+  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;PCData msg])
+let to_value f = function
+| Element ("value", attrs, l) ->
+  let ans = massoc "val" attrs in
+  if ans = "good" then Good (f (singleton l))
+  else if ans = "fail" then
+    let loc =
+      try
+        let loc_s = int_of_string (Serialize.massoc "loc_s" attrs) in
+        let loc_e = int_of_string (Serialize.massoc "loc_e" attrs) in
+        Some (loc_s, loc_e)
+      with Marshal_error | Failure _ -> None
+    in
+    let id = Stateid.of_xml (List.hd l) in
+    let msg = raw_string (List.tl l) in
+    Fail (id, loc, msg)
+  else raise Marshal_error
+| _ -> raise Marshal_error
+
+let of_status s =
+  let of_so = of_option of_string in
+  let of_sl = of_list of_string in
+  Element ("status", [], [
+      of_sl s.status_path;
+      of_so s.status_proofname;
+      of_sl s.status_allproofs;
+      of_int s.status_proofnum; ])
+let to_status = function
+  | Element ("status", [], [path; name; prfs; pnum]) -> {
+      status_path = to_list to_string path;
+      status_proofname = to_option to_string name;
+      status_allproofs = to_list to_string prfs;
+      status_proofnum = to_int pnum; }
+  | _ -> raise Marshal_error
+
+let of_evar s = Element ("evar", [], [PCData s.evar_info])
+let to_evar = function
+  | Element ("evar", [], data) -> { evar_info = raw_string data; }
+  | _ -> raise Marshal_error
+
+let of_goal g =
+  let hyp = of_list of_string g.goal_hyp in
+  let ccl = of_string 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 to_string hyp in
+    let ccl = to_string ccl in
+    let id = to_string id in
+    { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
+  | _ -> raise Marshal_error
+
+let of_goals g =
+  let of_glist = of_list of_goal in
+  let fg = of_list of_goal g.fg_goals in
+  let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
+  let shelf = of_list of_goal g.shelved_goals in
+  let given_up = of_list of_goal g.given_up_goals in
+  Element ("goals", [], [fg; bg; shelf; given_up])
+let to_goals = function
+  | Element ("goals", [], [fg; bg; shelf; given_up]) ->
+    let to_glist = to_list to_goal in
+    let fg = to_list to_goal fg in
+    let bg = to_list (to_pair to_glist to_glist) bg in
+    let shelf = to_list to_goal shelf in
+    let given_up = to_list to_goal given_up in
+    { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up }
+  | _ -> raise Marshal_error
+
+let of_coq_info info =
+  let version = of_string info.coqtop_version in
+  let protocol = of_string info.protocol_version in
+  let release = of_string info.release_date in
+  let compile = of_string info.compile_date in
+  Element ("coq_info", [], [version; protocol; release; compile])
+let to_coq_info = function
+  | Element ("coq_info", [], [version; protocol; release; compile]) -> {
+      coqtop_version = to_string version;
+      protocol_version = to_string protocol;
+      release_date = to_string release;
+      compile_date = to_string compile; }
+  | _ -> raise Marshal_error
+
+end
+include Xml_marshalling
+
+(* Reification of basic types and type constructors, and functions
+   from to xml *)
+module ReifType : sig
+
+  type 'a val_t
+
+  val unit_t         : unit val_t
+  val string_t       : string val_t
+  val int_t          : int val_t
+  val bool_t         : bool val_t
+  
+  val option_t       : 'a val_t -> 'a option val_t
+  val list_t         : 'a val_t -> 'a list val_t
+  val pair_t         : 'a val_t -> 'b val_t -> ('a * 'b) val_t
+  val union_t        : 'a val_t -> 'b val_t -> ('a ,'b) union val_t
+
+  val goals_t        : goals val_t
+  val evar_t         : evar val_t
+  val state_t        : status val_t
+  val option_state_t : option_state val_t
+  val option_value_t : option_value val_t
+  val coq_info_t     : coq_info val_t
+  val coq_object_t   : 'a val_t -> 'a coq_object val_t
+  val state_id_t     : state_id val_t
+  val search_cst_t   : search_constraint val_t
+
+  val of_value_type : 'a val_t -> 'a -> xml
+  val to_value_type : 'a val_t -> xml -> 'a
+
+  val print         : 'a val_t -> 'a -> string
+
+  type value_type
+  val erase         : 'a val_t -> value_type
+  val print_type    : value_type -> string
+
+  val document_type_encoding : (xml -> string) -> unit
+
+end = struct
+
+  type value_type =
+    | Unit | String | Int | Bool
+
+    | Option of value_type
+    | List of value_type
+    | Pair of value_type * value_type
+    | Union of value_type * value_type
+    
+    | Goals | Evar | State | Option_state | Option_value | Coq_info
+    | Coq_object of value_type
+    | State_id
+    | Search_cst
+
+  type 'a val_t = value_type
+  
+  let erase (x : 'a val_t) : value_type = x
+
+  let unit_t         = Unit
+  let string_t       = String
+  let int_t          = Int
+  let bool_t         = Bool
+
+  let option_t x     = Option x
+  let list_t x       = List x
+  let pair_t x y     = Pair (x, y)
+  let union_t x y    = Union (x, y)
+
+  let goals_t        = Goals
+  let evar_t         = Evar
+  let state_t        = State
+  let option_state_t = Option_state
+  let option_value_t = Option_value
+  let coq_info_t     = Coq_info
+  let coq_object_t x = Coq_object x
+  let state_id_t     = State_id
+  let search_cst_t   = Search_cst
+
+  let of_value_type (ty : 'a val_t) : 'a -> xml =
+    let rec convert ty : 'a -> xml = match ty with
+      | Unit          -> Obj.magic of_unit
+      | Bool          -> Obj.magic of_bool
+      | String        -> Obj.magic of_string
+      | Int           -> Obj.magic of_int
+      | State         -> Obj.magic of_status
+      | Option_state  -> Obj.magic of_option_state
+      | Option_value  -> Obj.magic of_option_value
+      | Coq_info      -> Obj.magic of_coq_info
+      | Goals         -> Obj.magic of_goals
+      | Evar          -> Obj.magic of_evar
+      | List t        -> Obj.magic (of_list (convert t))
+      | Option t      -> Obj.magic (of_option (convert t))
+      | Coq_object t  -> Obj.magic (of_coq_object (convert t))
+      | Pair (t1,t2)  -> Obj.magic (of_pair (convert t1) (convert t2))
+      | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
+      | State_id      -> Obj.magic Stateid.to_xml
+      | Search_cst    -> Obj.magic of_search_cst
+    in
+      convert ty
+  
+  let to_value_type (ty : 'a val_t) : xml -> 'a =
+    let rec convert ty : xml -> 'a = match ty with
+      | Unit          -> Obj.magic to_unit
+      | Bool          -> Obj.magic to_bool
+      | String        -> Obj.magic to_string
+      | Int           -> Obj.magic to_int
+      | State         -> Obj.magic to_status
+      | Option_state  -> Obj.magic to_option_state
+      | Option_value  -> Obj.magic to_option_value
+      | Coq_info      -> Obj.magic to_coq_info
+      | Goals         -> Obj.magic to_goals
+      | Evar          -> Obj.magic to_evar
+      | List t        -> Obj.magic (to_list (convert t))
+      | Option t      -> Obj.magic (to_option (convert t))
+      | Coq_object t  -> Obj.magic (to_coq_object (convert t))
+      | Pair (t1,t2)  -> Obj.magic (to_pair (convert t1) (convert t2))
+      | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
+      | State_id      -> Obj.magic Stateid.of_xml
+      | Search_cst    -> Obj.magic to_search_cst
+    in
+      convert ty
+
+  let pr_unit () = ""
+  let pr_string s = Printf.sprintf "%S" s
+  let pr_int i = string_of_int i
+  let pr_bool b = Printf.sprintf "%B" b
+  let pr_goal (g : goals) =
+    if g.fg_goals = [] then
+      if g.bg_goals = [] then "Proof completed."
+      else
+        let rec pr_focus _ = function
+          | [] -> assert false
+          | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
+          | (lg, rg) :: l ->
+            Printf.sprintf "%i:%a"
+              (List.length lg + List.length rg) pr_focus l in
+        Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+    else
+      let pr_menu s = s in
+      let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
+        "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^
+            pr_menu goal ^ "]" in
+      String.concat " " (List.map pr_goal g.fg_goals)
+  let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
+  let pr_status (s : status) =
+    let path =
+      let l = String.concat "." s.status_path in
+      "path=" ^ l ^ ";" in
+    let name = match s.status_proofname with
+      | None -> "no proof;"
+      | Some n -> "proof = " ^ n ^ ";" in
+    "Status: " ^ path ^ name
+  let pr_coq_info (i : coq_info) = "FIXME"
+  let pr_option_value = function
+    | IntValue None -> "none"
+    | IntValue (Some i) -> string_of_int i
+    | StringValue s -> s
+    | BoolValue b -> if b then "true" else "false"
+  let pr_option_state (s : option_state) =
+    Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
+      s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+  let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
+  let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
+  let pr_coq_object (o : 'a coq_object) = "FIXME"
+  let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")"
+  let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x
+
+  let pr_search_cst = function
+    | Name_Pattern s -> "Name_Pattern " ^ s
+    | Type_Pattern s -> "Type_Pattern " ^ s
+    | SubType_Pattern s -> "SubType_Pattern " ^ s
+    | In_Module s -> "In_Module " ^ String.concat "." s
+    | Include_Blacklist -> "Include_Blacklist"
+
+  let rec print = function
+  | Unit          -> Obj.magic pr_unit
+  | Bool          -> Obj.magic pr_bool
+  | String        -> Obj.magic pr_string
+  | Int           -> Obj.magic pr_int
+  | State         -> Obj.magic pr_status
+  | Option_state  -> Obj.magic pr_option_state
+  | Option_value  -> Obj.magic pr_option_value
+  | Search_cst    -> Obj.magic pr_search_cst
+  | Coq_info      -> Obj.magic pr_coq_info
+  | Goals         -> Obj.magic pr_goal
+  | Evar          -> Obj.magic pr_evar
+  | List t        -> Obj.magic (pr_list (print t))
+  | Option t      -> Obj.magic (pr_option (print t))
+  | Coq_object t  -> Obj.magic pr_coq_object
+  | Pair (t1,t2)  -> Obj.magic (pr_pair (print t1) (print t2))
+  | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2))
+  | State_id      -> Obj.magic pr_int
+
+  (* This is to break if a rename/refactoring makes the strings below outdated *)
+  type 'a exists = bool
+
+  let rec print_type = function
+  | Unit          -> "unit"
+  | Bool          -> "bool"
+  | String        -> "string"
+  | Int           -> "int"
+  | State         -> assert(true : status exists); "Interface.status"
+  | Option_state  -> assert(true : option_state exists); "Interface.option_state"
+  | Option_value  -> assert(true : option_value exists); "Interface.option_value"
+  | Search_cst    -> assert(true : search_constraint exists); "Interface.search_constraint"
+  | Coq_info      -> assert(true : coq_info exists); "Interface.coq_info"
+  | Goals         -> assert(true : goals exists); "Interface.goals"
+  | Evar          -> assert(true : evar exists); "Interface.evar"
+  | List t        -> Printf.sprintf "(%s list)" (print_type t)
+  | Option t      -> Printf.sprintf "(%s option)" (print_type t)
+  | Coq_object t  -> assert(true : 'a coq_object exists);
+                     Printf.sprintf "(%s Interface.coq_object)" (print_type t)
+  | Pair (t1,t2)  -> Printf.sprintf "(%s * %s)" (print_type t1) (print_type t2)
+  | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists);
+                     Printf.sprintf "((%s, %s) CSig.union)" (print_type t1) (print_type t2)
+  | State_id      -> assert(true : Stateid.t exists); "Stateid.t"
+
+  let document_type_encoding pr_xml =
+    Printf.printf "\n=== Data encoding by examples ===\n\n";
+    Printf.printf "%s:\n\n%s\n\n" (print_type Unit) (pr_xml (of_unit ()));
+    Printf.printf "%s:\n\n%s\n%s\n\n" (print_type Bool)
+      (pr_xml (of_bool true)) (pr_xml (of_bool false));
+    Printf.printf "%s:\n\n%s\n\n" (print_type String) (pr_xml (of_string "hello"));
+    Printf.printf "%s:\n\n%s\n\n" (print_type Int) (pr_xml (of_int 256));
+    Printf.printf "%s:\n\n%s\n\n" (print_type State_id) (pr_xml (Stateid.to_xml Stateid.initial));
+    Printf.printf "%s:\n\n%s\n\n" (print_type (List Int)) (pr_xml (of_list of_int [3;4;5]));
+    Printf.printf "%s:\n\n%s\n%s\n\n" (print_type (Option Int))
+      (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None));
+    Printf.printf "%s:\n\n%s\n\n" (print_type (Pair (Bool,Int)))
+      (pr_xml (of_pair of_bool of_int (false,3)));
+    Printf.printf "%s:\n\n%s\n\n" (print_type (Union (Bool,Int)))
+      (pr_xml (of_union of_bool of_int (Inl false)));
+    print_endline ("All other types are records represented by a node named like the OCaml\n"^
+                   "type which contains a flattened n-tuple.  We provide one example.\n");
+    Printf.printf "%s:\n\n%s\n\n" (print_type Option_state)
+      (pr_xml (of_option_state { opt_sync = true; opt_depr = false;
+        opt_name = "name1"; opt_value = IntValue (Some 37) }));
+
+end
+open ReifType
+
+(** Types reification, checked with explicit casts *)
+let add_sty_t : add_sty val_t = 
+  pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t)
+let edit_at_sty_t : edit_at_sty val_t = state_id_t
+let query_sty_t : query_sty val_t = pair_t string_t state_id_t
+let goals_sty_t : goals_sty val_t = unit_t
+let evars_sty_t : evars_sty val_t = unit_t
+let hints_sty_t : hints_sty val_t = unit_t
+let status_sty_t : status_sty val_t = bool_t
+let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t)
+let get_options_sty_t : get_options_sty val_t = unit_t
+let set_options_sty_t : set_options_sty val_t =
+  list_t (pair_t (list_t string_t) option_value_t)
+let mkcases_sty_t : mkcases_sty val_t = string_t
+let quit_sty_t : quit_sty val_t = unit_t
+let about_sty_t : about_sty val_t = unit_t
+let init_sty_t : init_sty val_t = option_t string_t
+let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
+let stop_worker_sty_t : stop_worker_sty val_t = int_t
+
+let add_rty_t : add_rty val_t =
+  pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
+let edit_at_rty_t : edit_at_rty val_t =
+  union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t))
+let query_rty_t : query_rty val_t = string_t
+let goals_rty_t : goals_rty val_t = option_t goals_t
+let evars_rty_t : evars_rty val_t = option_t (list_t evar_t)
+let hints_rty_t : hints_rty val_t =
+  let hint = list_t (pair_t string_t string_t) in
+  option_t (pair_t (list_t hint) hint)
+let status_rty_t : status_rty val_t = state_t
+let search_rty_t : search_rty val_t = list_t (coq_object_t string_t)
+let get_options_rty_t : get_options_rty val_t =
+  list_t (pair_t (list_t string_t) option_state_t) 
+let set_options_rty_t : set_options_rty val_t = unit_t
+let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t)
+let quit_rty_t : quit_rty val_t = unit_t
+let about_rty_t : about_rty val_t = coq_info_t
+let init_rty_t : init_rty val_t = state_id_t
+let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t)
+let stop_worker_rty_t : stop_worker_rty val_t = unit_t
+
+let ($) x = erase x
+let calls = [|  
+  "Add",        ($)add_sty_t,         ($)add_rty_t;
+  "Edit_at",    ($)edit_at_sty_t,     ($)edit_at_rty_t;
+  "Query",      ($)query_sty_t,       ($)query_rty_t;
+  "Goal",       ($)goals_sty_t,       ($)goals_rty_t;
+  "Evars",      ($)evars_sty_t,       ($)evars_rty_t;
+  "Hints",      ($)hints_sty_t,       ($)hints_rty_t;
+  "Status",     ($)status_sty_t,      ($)status_rty_t;
+  "Search",     ($)search_sty_t,      ($)search_rty_t;
+  "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t;
+  "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t;
+  "MkCases",    ($)mkcases_sty_t,     ($)mkcases_rty_t;
+  "Quit",       ($)quit_sty_t,        ($)quit_rty_t;
+  "About",      ($)about_sty_t,       ($)about_rty_t;
+  "Init",       ($)init_sty_t,        ($)init_rty_t;
+  "Interp",     ($)interp_sty_t,      ($)interp_rty_t;
+  "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t;
+|]
+
+type 'a call =
+  | Add        of add_sty
+  | Edit_at    of edit_at_sty
+  | Query      of query_sty
+  | Goal       of goals_sty
+  | Evars      of evars_sty
+  | Hints      of hints_sty
+  | Status     of status_sty
+  | Search     of search_sty
+  | GetOptions of get_options_sty
+  | SetOptions of set_options_sty
+  | MkCases    of mkcases_sty
+  | Quit       of quit_sty
+  | About      of about_sty
+  | Init       of init_sty
+  | StopWorker of stop_worker_sty
+  (* retrocompatibility *)
+  | Interp     of interp_sty
+
+let id_of_call = function
+  | Add _        -> 0
+  | Edit_at _    -> 1
+  | Query _      -> 2
+  | Goal _       -> 3
+  | Evars _      -> 4
+  | Hints _      -> 5
+  | Status _     -> 6
+  | Search _     -> 7
+  | GetOptions _ -> 8
+  | SetOptions _ -> 9
+  | MkCases _    -> 10
+  | Quit _       -> 11
+  | About _      -> 12
+  | Init _       -> 13
+  | Interp _     -> 14
+  | StopWorker _ -> 15
+
+let str_of_call c = pi1 calls.(id_of_call c)
+
+type unknown
+
+(** We use phantom types and GADT to protect ourselves against wild casts *)
+let add x         : add_rty call         = Add x
+let edit_at x     : edit_at_rty call     = Edit_at x
+let query x       : query_rty call       = Query x
+let goals x       : goals_rty call       = Goal x
+let evars x       : evars_rty call       = Evars x
+let hints x       : hints_rty call       = Hints x
+let status x      : status_rty call      = Status x
+let get_options x : get_options_rty call = GetOptions x
+let set_options x : set_options_rty call = SetOptions x
+let mkcases x     : mkcases_rty call     = MkCases x
+let search x      : search_rty call      = Search x
+let quit x        : quit_rty call        = Quit x
+let init x        : init_rty call        = Init x
+let interp x      : interp_rty call      = Interp x
+let stop_worker x : stop_worker_rty call = StopWorker x
+
+let abstract_eval_call handler (c : 'a call) : 'a value =
+  let mkGood x : 'a value = Good (Obj.magic x) in
+  try
+    match c with
+    | Add x        -> mkGood (handler.add x)
+    | Edit_at x    -> mkGood (handler.edit_at x)
+    | Query x      -> mkGood (handler.query x)
+    | Goal x       -> mkGood (handler.goals x)
+    | Evars x      -> mkGood (handler.evars x)
+    | Hints x      -> mkGood (handler.hints x)
+    | Status x     -> mkGood (handler.status x)
+    | Search x     -> mkGood (handler.search x)
+    | GetOptions x -> mkGood (handler.get_options x)
+    | SetOptions x -> mkGood (handler.set_options x)
+    | MkCases x    -> mkGood (handler.mkcases x)
+    | Quit x       -> mkGood (handler.quit x)
+    | About x      -> mkGood (handler.about x)
+    | Init x       -> mkGood (handler.init x)
+    | Interp x     -> mkGood (handler.interp x)
+    | StopWorker x -> mkGood (handler.stop_worker x)
+  with any ->
+    Fail (handler.handle_exn any)
+
+(** brain dead code, edit if protocol messages are added/removed *)
+let of_answer (q : 'a call) (v : 'a value) : xml = match q with
+  | Add _        -> of_value (of_value_type add_rty_t        ) (Obj.magic v)
+  | Edit_at _    -> of_value (of_value_type edit_at_rty_t    ) (Obj.magic v)
+  | Query _      -> of_value (of_value_type query_rty_t      ) (Obj.magic v)
+  | Goal _       -> of_value (of_value_type goals_rty_t      ) (Obj.magic v)
+  | Evars _      -> of_value (of_value_type evars_rty_t      ) (Obj.magic v)
+  | Hints _      -> of_value (of_value_type hints_rty_t      ) (Obj.magic v)
+  | Status _     -> of_value (of_value_type status_rty_t     ) (Obj.magic v)
+  | Search _     -> of_value (of_value_type search_rty_t     ) (Obj.magic v)
+  | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v)
+  | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v)
+  | MkCases _    -> of_value (of_value_type mkcases_rty_t    ) (Obj.magic v)
+  | Quit _       -> of_value (of_value_type quit_rty_t       ) (Obj.magic v)
+  | About _      -> of_value (of_value_type about_rty_t      ) (Obj.magic v)
+  | Init _       -> of_value (of_value_type init_rty_t       ) (Obj.magic v)
+  | Interp _     -> of_value (of_value_type interp_rty_t     ) (Obj.magic v)
+  | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v)
+
+let to_answer (q : 'a call) (x : xml) : 'a value = match q with
+  | Add _        -> Obj.magic (to_value (to_value_type add_rty_t        ) x)
+  | Edit_at _    -> Obj.magic (to_value (to_value_type edit_at_rty_t    ) x)
+  | Query _      -> Obj.magic (to_value (to_value_type query_rty_t      ) x)
+  | Goal _       -> Obj.magic (to_value (to_value_type goals_rty_t      ) x)
+  | Evars _      -> Obj.magic (to_value (to_value_type evars_rty_t      ) x)
+  | Hints _      -> Obj.magic (to_value (to_value_type hints_rty_t      ) x)
+  | Status _     -> Obj.magic (to_value (to_value_type status_rty_t     ) x)
+  | Search _     -> Obj.magic (to_value (to_value_type search_rty_t     ) x)
+  | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x)
+  | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x)
+  | MkCases _    -> Obj.magic (to_value (to_value_type mkcases_rty_t    ) x)
+  | Quit _       -> Obj.magic (to_value (to_value_type quit_rty_t       ) x)
+  | About _      -> Obj.magic (to_value (to_value_type about_rty_t      ) x)
+  | Init _       -> Obj.magic (to_value (to_value_type init_rty_t       ) x)
+  | Interp _     -> Obj.magic (to_value (to_value_type interp_rty_t     ) x)
+  | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x)
+
+let of_call (q : 'a call) : xml =
+  let mkCall x = constructor "call" (str_of_call q) [x] in
+  match q with
+  | Add x        -> mkCall (of_value_type add_sty_t         x) 
+  | Edit_at x    -> mkCall (of_value_type edit_at_sty_t     x) 
+  | Query x      -> mkCall (of_value_type query_sty_t       x) 
+  | Goal x       -> mkCall (of_value_type goals_sty_t       x) 
+  | Evars x      -> mkCall (of_value_type evars_sty_t       x) 
+  | Hints x      -> mkCall (of_value_type hints_sty_t       x) 
+  | Status x     -> mkCall (of_value_type status_sty_t      x) 
+  | Search x     -> mkCall (of_value_type search_sty_t      x) 
+  | GetOptions x -> mkCall (of_value_type get_options_sty_t x) 
+  | SetOptions x -> mkCall (of_value_type set_options_sty_t x) 
+  | MkCases x    -> mkCall (of_value_type mkcases_sty_t     x) 
+  | Quit x       -> mkCall (of_value_type quit_sty_t        x) 
+  | About x      -> mkCall (of_value_type about_sty_t       x) 
+  | Init x       -> mkCall (of_value_type init_sty_t        x)
+  | Interp x     -> mkCall (of_value_type interp_sty_t      x)
+  | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x)
+
+let to_call : xml -> unknown call =
+  do_match "call" (fun s a ->
+    let mkCallArg vt a = to_value_type vt (singleton a) in
+    match s with
+    | "Add"        -> Add        (mkCallArg add_sty_t         a)
+    | "Edit_at"    -> Edit_at    (mkCallArg edit_at_sty_t     a)
+    | "Query"      -> Query      (mkCallArg query_sty_t       a)
+    | "Goal"       -> Goal       (mkCallArg goals_sty_t       a)
+    | "Evars"      -> Evars      (mkCallArg evars_sty_t       a)
+    | "Hints"      -> Hints      (mkCallArg hints_sty_t       a)
+    | "Status"     -> Status     (mkCallArg status_sty_t      a)
+    | "Search"     -> Search     (mkCallArg search_sty_t      a)
+    | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a)
+    | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a)
+    | "MkCases"    -> MkCases    (mkCallArg mkcases_sty_t     a)
+    | "Quit"       -> Quit       (mkCallArg quit_sty_t        a)
+    | "About"      -> About      (mkCallArg about_sty_t       a)
+    | "Init"       -> Init       (mkCallArg init_sty_t        a)
+    | "Interp"     -> Interp     (mkCallArg interp_sty_t      a)
+    | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a)
+    | _ -> raise Marshal_error)
+
+(** Debug printing *)
+
+let pr_value_gen pr = function
+  | Good v -> "GOOD " ^ pr v
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]"
+  | Fail (id,Some(i,j),str) ->
+      "FAIL "^Stateid.to_string id^
+        " ("^string_of_int i^","^string_of_int j^")["^str^"]"
+let pr_value v = pr_value_gen (fun _ -> "FIXME") v
+let pr_full_value call value = match call with
+  | Add _        -> pr_value_gen (print add_rty_t        ) (Obj.magic value) 
+  | Edit_at _    -> pr_value_gen (print edit_at_rty_t    ) (Obj.magic value) 
+  | Query _      -> pr_value_gen (print query_rty_t      ) (Obj.magic value) 
+  | Goal _       -> pr_value_gen (print goals_rty_t      ) (Obj.magic value) 
+  | Evars _      -> pr_value_gen (print evars_rty_t      ) (Obj.magic value) 
+  | Hints _      -> pr_value_gen (print hints_rty_t      ) (Obj.magic value) 
+  | Status _     -> pr_value_gen (print status_rty_t     ) (Obj.magic value) 
+  | Search _     -> pr_value_gen (print search_rty_t     ) (Obj.magic value) 
+  | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) 
+  | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) 
+  | MkCases _    -> pr_value_gen (print mkcases_rty_t    ) (Obj.magic value) 
+  | Quit _       -> pr_value_gen (print quit_rty_t       ) (Obj.magic value) 
+  | About _      -> pr_value_gen (print about_rty_t      ) (Obj.magic value) 
+  | Init _       -> pr_value_gen (print init_rty_t       ) (Obj.magic value)
+  | Interp _     -> pr_value_gen (print interp_rty_t     ) (Obj.magic value)
+  | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value)
+let pr_call call = match call with
+  | Add x        -> str_of_call call ^ " " ^ print add_sty_t         x
+  | Edit_at x    -> str_of_call call ^ " " ^ print edit_at_sty_t     x
+  | Query x      -> str_of_call call ^ " " ^ print query_sty_t       x
+  | Goal x       -> str_of_call call ^ " " ^ print goals_sty_t       x
+  | Evars x      -> str_of_call call ^ " " ^ print evars_sty_t       x
+  | Hints x      -> str_of_call call ^ " " ^ print hints_sty_t       x
+  | Status x     -> str_of_call call ^ " " ^ print status_sty_t      x
+  | Search x     -> str_of_call call ^ " " ^ print search_sty_t      x
+  | GetOptions x -> str_of_call call ^ " " ^ print get_options_sty_t x
+  | SetOptions x -> str_of_call call ^ " " ^ print set_options_sty_t x
+  | MkCases x    -> str_of_call call ^ " " ^ print mkcases_sty_t     x
+  | Quit x       -> str_of_call call ^ " " ^ print quit_sty_t        x
+  | About x      -> str_of_call call ^ " " ^ print about_sty_t       x
+  | Init x       -> str_of_call call ^ " " ^ print init_sty_t        x
+  | Interp x     -> str_of_call call ^ " " ^ print interp_sty_t      x
+  | StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x
+
+let document to_string_fmt =
+  Printf.printf "=== Available calls ===\n\n";
+  Array.iter (fun (cname, csty, crty) ->
+      Printf.printf "%12s :  %s\n %14s %s\n"
+        ("\""^cname^"\"") (print_type csty) "->" (print_type crty))
+    calls;
+  Printf.printf "\n=== Calls XML encoding ===\n\n";
+  Printf.printf "A call \"C\" carrying input a is encoded as:\n\n%s\n\n"
+    (to_string_fmt (constructor "call" "C" [PCData "a"]));
+  Printf.printf "A response carrying output b can either be:\n\n%s\n\n"
+    (to_string_fmt (of_value (fun _ -> PCData "b") (Good ())));
+  Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n"
+    (to_string_fmt (of_value (fun _ -> PCData "b")
+      (Fail (Stateid.initial,Some (15,34),"error message"))));
+  document_type_encoding to_string_fmt
+
+(* vim: set foldmethod=marker: *)
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
new file mode 100644
index 000000000..42defce85
--- /dev/null
+++ b/ide/xmlprotocol.mli
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Applicative part of the interface of CoqIde calls to Coq *)
+
+open Interface
+open Xml_datatype
+
+type 'a call
+
+type unknown
+
+val add         : add_sty         -> add_rty call
+val edit_at     : edit_at_sty     -> edit_at_rty call
+val query       : query_sty       -> query_rty call
+val goals       : goals_sty       -> goals_rty call
+val hints       : hints_sty       -> hints_rty call
+val status      : status_sty      -> status_rty call
+val mkcases     : mkcases_sty     -> mkcases_rty call
+val evars       : evars_sty       -> evars_rty call
+val search      : search_sty      -> search_rty call
+val get_options : get_options_sty -> get_options_rty call
+val set_options : set_options_sty -> set_options_rty call
+val quit        : quit_sty        -> quit_rty call
+val init        : init_sty        -> init_rty call
+val stop_worker : stop_worker_sty -> stop_worker_rty call
+(* retrocompatibility *)
+val interp      : interp_sty      -> interp_rty call
+
+val abstract_eval_call : handler -> 'a call -> 'a value
+
+(** * Protocol version *)
+
+val protocol_version : string
+
+(** * XML data marshalling *)
+
+val of_call : 'a call -> xml
+val to_call : xml -> unknown call
+
+val of_answer : 'a call -> 'a value -> xml
+val to_answer : 'a call -> xml -> 'a value
+
+(* Prints the documentation of this module *)
+val document : (xml -> string) -> unit
+
+(** * Debug printing *)
+
+val pr_call : 'a call -> string
+val pr_value : 'a value -> string
+val pr_full_value : 'a call -> 'a value -> string
diff --git a/idetop/coqidetop.mllib b/idetop/coqidetop.mllib
deleted file mode 100644
index 782687744..000000000
--- a/idetop/coqidetop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Ide_slave
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 80b5830fd..bf9d2c0b9 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -131,7 +131,7 @@ let interval loc =
 
 let dump_ref loc filepath modpath ident ty =
   if !glob_output = Feedback then
-    Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty))
+    Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
   else
     let bl,el = interval loc in
     dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
@@ -229,7 +229,7 @@ let dump_binding loc id = ()
 
 let dump_def ty loc secpath id =
   if !glob_output = Feedback then
-    Pp.feedback (Interface.GlobDef (loc, id, secpath, ty))
+    Pp.feedback (Feedback.GlobDef (loc, id, secpath, ty))
   else
     let bl,el = interval loc in
     dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 89e1b41f3..af65f6541 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -148,7 +148,7 @@ type obsolete_locality = bool
  * compatible.  If the grammar is fixed removing deprecated syntax, this
  * bool should go away too *)
 
-type option_value = Interface.option_value =
+type option_value = Goptions.option_value =
   | BoolValue of bool
   | IntValue of int option
   | StringValue of string
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f38ad4742..9f30b7da3 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -105,7 +105,7 @@ let hcons_j j =
   { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
 
 let feedback_completion_typecheck =
-  Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete)
+  Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
 
 let check_projection env kn inst body =
   let cannot_recognize () = error ("Cannot recognize a projection") in
diff --git a/lib/clib.mllib b/lib/clib.mllib
index ed4894cb9..73839fd9e 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -17,6 +17,8 @@ IStream
 Pp_control
 Flags
 Control
+Loc
+Serialize
 Pp
 Deque
 CObj
@@ -25,9 +27,8 @@ CString
 CArray
 CStack
 Util
-Loc
 Stateid
-Serialize
+Feedback
 CUnix
 Envars
 Aux_file
diff --git a/lib/feedback.ml b/lib/feedback.ml
new file mode 100644
index 000000000..b532c2653
--- /dev/null
+++ b/lib/feedback.ml
@@ -0,0 +1,96 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Xml_datatype
+open Serialize
+
+type edit_id = int
+type state_id = Stateid.t
+type edit_or_state_id = Edit of edit_id | State of state_id
+
+type feedback_content =
+  | AddedAxiom
+  | Processed
+  | Incomplete
+  | Complete
+  | GlobRef of Loc.t * string * string * string * string
+  | GlobDef of Loc.t * string * string * string
+  | ErrorMsg of Loc.t * string
+  | InProgress of int
+  | SlaveStatus of int * string
+  | ProcessingInMaster
+
+type feedback = {
+  id : edit_or_state_id;
+  content : feedback_content;
+}
+
+let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
+  | "addedaxiom", _ -> AddedAxiom
+  | "processed", _ -> Processed
+  | "processinginmaster", _ -> ProcessingInMaster
+  | "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)
+  | "slavestatus", [ns] ->
+       let n, s = to_pair to_int to_string ns in
+       SlaveStatus(n,s)
+  | _ -> raise Marshal_error)
+let of_feedback_content = function
+  | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
+  | Processed -> constructor "feedback_content" "processed" []
+  | ProcessingInMaster -> constructor "feedback_content" "processinginmaster" []
+  | 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]
+  | SlaveStatus(n,s) ->
+      constructor "feedback_content" "slavestatus"
+        [of_pair of_int of_string (n,s)]
+
+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.content in
+  let obj, id = of_edit_or_state_id msg.id in
+  Element ("feedback", obj, [id;content])
+let to_feedback xml = match xml with
+  | Element ("feedback", ["object","edit"], [id;content]) -> {
+      id = Edit(to_edit_id id);
+      content = to_feedback_content content }
+  | Element ("feedback", ["object","state"], [id;content]) -> { 
+      id = State(Stateid.of_xml id);
+      content = to_feedback_content content }
+  | _ -> raise Marshal_error
+
+let is_feedback = function
+  | Element ("feedback", _, _) -> true
+  | _ -> false
+
diff --git a/lib/feedback.mli b/lib/feedback.mli
new file mode 100644
index 000000000..e7645ca16
--- /dev/null
+++ b/lib/feedback.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Xml_datatype
+
+(** 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 feedback_content =
+  | AddedAxiom
+  | Processed
+  | Incomplete
+  | Complete
+  | GlobRef of Loc.t * string * string * string * string
+  | GlobDef of Loc.t * string * string * string
+  | ErrorMsg of Loc.t * string
+  | InProgress of int
+  | SlaveStatus of int * string
+  | ProcessingInMaster
+
+type feedback = {
+  id : edit_or_state_id;
+  content : feedback_content;
+}
+
+val of_feedback : feedback -> xml
+val to_feedback : xml -> feedback
+val is_feedback : xml -> bool
+
diff --git a/lib/pp.ml b/lib/pp.ml
index f9fe53fdf..91ea5230d 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -345,14 +345,49 @@ let msgerrnl x = msgnl_with !err_ft x
 
 (* Logging management *)
 
-type level = Interface.message_level =
-| Debug of string
-| Info
-| Notice
-| Warning
-| Error
-
-type logger = level -> std_ppcmds -> unit
+type message_level =
+  | Debug of string
+  | Info
+  | Notice
+  | Warning
+  | Error
+
+type message = {
+  message_level : message_level;
+  message_content : string;
+}
+
+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_string 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_string content }
+  | _ -> raise Serialize.Marshal_error
+
+let is_message = function
+  | Xml_datatype.Element ("message", _, _) -> true
+  | _ -> false
+
+type logger = message_level -> std_ppcmds -> unit
 
 let print_color s x = x
 (* FIXME *)
@@ -387,14 +422,14 @@ let set_logger l = logger := l
 (** Feedback *)
 
 let feeder = ref ignore
-let feedback_id = ref (Interface.Edit 0)
+let feedback_id = ref (Feedback.Edit 0)
 let set_id_for_feedback i = feedback_id := i
 let feedback ?state_id what =
   !feeder {
-     Interface.content = what;
-     Interface.id =
+     Feedback.content = what;
+     Feedback.id =
        match state_id with
-       | Some id -> Interface.State id
+       | Some id -> Feedback.State id
        | None -> !feedback_id;
   }
 let set_feeder f = feeder := f
diff --git a/lib/pp.mli b/lib/pp.mli
index 635a149e8..fe11619c1 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -78,8 +78,19 @@ val close : unit -> std_ppcmds
 val tclose : unit -> std_ppcmds
 
 (** {6 Sending messages to the user} *)
+type message_level =
+  | Debug of string
+  | Info
+  | Notice
+  | Warning
+  | Error
 
-type logger = Interface.message_level -> std_ppcmds -> unit
+type message = {
+  message_level : message_level;
+  message_content : string;
+}
+
+type logger = message_level -> std_ppcmds -> unit
 
 val msg_info : std_ppcmds -> unit
 (** Message that displays information, usually in verbose mode, such as [Foobar
@@ -104,6 +115,11 @@ val std_logger : logger
 
 val set_logger : logger -> unit
 
+val of_message : message -> Xml_datatype.xml
+val to_message : Xml_datatype.xml -> message
+val is_message : Xml_datatype.xml -> bool
+
+
 (** {6 Feedback sent, even asynchronously, to the user interface} *)
 
 (* This stuff should be available to most of the system, line msg_* above.
@@ -116,10 +132,10 @@ val set_logger : logger -> unit
  * since the two phases are performed sequentially) *)
 
 val feedback :
-  ?state_id:Interface.state_id -> Interface.feedback_content -> unit
+  ?state_id:Feedback.state_id -> Feedback.feedback_content -> unit
 
-val set_id_for_feedback : Interface.edit_or_state_id -> unit
-val set_feeder : (Interface.feedback -> unit) -> unit
+val set_id_for_feedback : Feedback.edit_or_state_id -> unit
+val set_feeder : (Feedback.feedback -> unit) -> unit
 
 (** {6 Utilities} *)
 
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 042b75e2d..7c0c6b86e 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -6,21 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Protocol version of this file. This is the date of the last modification. *)
-
-(** WARNING: TO BE UPDATED WHEN MODIFIED! *)
-
-let protocol_version = "20140312"
-
-(** * Interface of calls to Coq by CoqIde *)
-
-open Util
-open Interface
 open Xml_datatype
 
-(* Marshalling of basic types and type constructors *)
-module Xml_marshalling = struct
-
 exception Marshal_error
 
 (** Utility functions *)
@@ -96,76 +83,16 @@ let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
   | Element ("pair", [], [x; y]) -> (f x, g y)
   | _ -> raise Marshal_error
 
-let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) union -> xml = function
-  | Inl x -> Element ("union", ["val","in_l"], [f x])
-  | Inr x -> Element ("union", ["val","in_r"], [g x])
-let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) union = function
-  | Element ("union", ["val","in_l"], [x]) -> Inl (f x)
-  | Element ("union", ["val","in_r"], [x]) -> Inr (g x)
+let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function
+  | CSig.Inl x -> Element ("union", ["val","in_l"], [f x])
+  | CSig.Inr x -> Element ("union", ["val","in_r"], [g x])
+let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function
+  | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x)
+  | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x)
   | _ -> raise Marshal_error
 
 (** More elaborate types *)
 
-let of_option_value = function
-  | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i]
-  | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b]
-  | StringValue s -> constructor "option_value" "stringvalue" [of_string s]
-let to_option_value = do_match "option_value" (fun s args -> match s with
-  | "intvalue" -> IntValue (to_option to_int (singleton args))
-  | "boolvalue" -> BoolValue (to_bool (singleton args))
-  | "stringvalue" -> StringValue (to_string (singleton args))
-  | _ -> raise Marshal_error)
-
-let of_option_state s =
-  Element ("option_state", [], [
-    of_bool s.opt_sync;
-    of_bool s.opt_depr;
-    of_string s.opt_name;
-    of_option_value s.opt_value])
-let to_option_state = function
-  | Element ("option_state", [], [sync; depr; name; value]) -> {
-      opt_sync = to_bool sync;
-      opt_depr = to_bool depr;
-      opt_name = to_string name;
-      opt_value = to_option_value value }
-  | _ -> raise Marshal_error
-
-let of_search_cst = function
-  | Name_Pattern s ->
-    constructor "search_cst" "name_pattern" [of_string s]
-  | Type_Pattern s ->
-    constructor "search_cst" "type_pattern" [of_string s]
-  | SubType_Pattern s ->
-    constructor "search_cst" "subtype_pattern" [of_string s]
-  | In_Module m ->
-    constructor "search_cst" "in_module" [of_list of_string m]
-  | Include_Blacklist ->
-    constructor "search_cst" "include_blacklist" []
-let to_search_cst = do_match "search_cst" (fun s args -> match s with
-  | "name_pattern" -> Name_Pattern (to_string (singleton args))
-  | "type_pattern" -> Type_Pattern (to_string (singleton args))
-  | "subtype_pattern" -> SubType_Pattern (to_string (singleton args))
-  | "in_module" -> In_Module (to_list to_string (singleton args))
-  | "include_blacklist" -> Include_Blacklist
-  | _ -> raise Marshal_error)
-
-let of_coq_object f ans =
-  let prefix = of_list of_string ans.coq_object_prefix in
-  let qualid = of_list of_string ans.coq_object_qualid in
-  let obj = f ans.coq_object_object in
-  Element ("coq_object", [], [prefix; qualid; obj])
-
-let to_coq_object f = function
-| Element ("coq_object", [], [prefix; qualid; obj]) ->
-  let prefix = to_list to_string prefix in
-  let qualid = to_list to_string qualid in
-  let obj = f obj in {
-    coq_object_prefix = prefix;
-    coq_object_qualid = qualid;
-    coq_object_object = obj;
-  }
-| _ -> raise Marshal_error
-
 let of_edit_id i = Element ("edit_id",["val",string_of_int i],[])
 let to_edit_id = function
   | Element ("edit_id",["val",i],[]) ->
@@ -174,138 +101,11 @@ let to_edit_id = function
       id
   | _ -> raise Marshal_error
 
-let of_state_id id =
-  try Stateid.to_xml id with Invalid_argument _ -> raise Marshal_error
-let to_state_id xml =
-  try Stateid.of_xml xml with Invalid_argument _ -> raise Marshal_error
-
-let of_edit_or_state_id = function
-  | Interface.Edit id -> ["object","edit"], of_edit_id id
-  | Interface.State id -> ["object","state"], of_state_id id
-
-let of_value f = function
-| Good x -> Element ("value", ["val", "good"], [f x])
-| Fail (id,loc, msg) ->
-  let loc = match loc with
-  | None -> []
-  | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
-  let id = of_state_id id in
-  Element ("value", ["val", "fail"] @ loc, [id;PCData msg])
-let to_value f = function
-| Element ("value", attrs, l) ->
-  let ans = massoc "val" attrs in
-  if ans = "good" then Good (f (singleton l))
-  else if ans = "fail" then
-    let loc =
-      try
-        let loc_s = int_of_string (get_attr "loc_s" attrs) in
-        let loc_e = int_of_string (get_attr "loc_e" attrs) in
-        Some (loc_s, loc_e)
-      with Not_found | Failure _ -> None
-    in
-    let id = to_state_id (List.hd l) in
-    let msg = raw_string (List.tl l) in
-    Fail (id, loc, msg)
-  else raise Marshal_error
-| _ -> raise Marshal_error
-
-let of_status s =
-  let of_so = of_option of_string in
-  let of_sl = of_list of_string in
-  Element ("status", [], [
-      of_sl s.status_path;
-      of_so s.status_proofname;
-      of_sl s.status_allproofs;
-      of_int s.status_proofnum; ])
-let to_status = function
-  | Element ("status", [], [path; name; prfs; pnum]) -> {
-      status_path = to_list to_string path;
-      status_proofname = to_option to_string name;
-      status_allproofs = to_list to_string prfs;
-      status_proofnum = to_int pnum; }
-  | _ -> raise Marshal_error
-
-let of_evar s = Element ("evar", [], [PCData s.evar_info])
-let to_evar = function
-  | Element ("evar", [], data) -> { evar_info = raw_string data; }
-  | _ -> raise Marshal_error
-
-let of_goal g =
-  let hyp = of_list of_string g.goal_hyp in
-  let ccl = of_string 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 to_string hyp in
-    let ccl = to_string ccl in
-    let id = to_string id in
-    { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
-  | _ -> raise Marshal_error
-
-let of_goals g =
-  let of_glist = of_list of_goal in
-  let fg = of_list of_goal g.fg_goals in
-  let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
-  let shelf = of_list of_goal g.shelved_goals in
-  let given_up = of_list of_goal g.given_up_goals in
-  Element ("goals", [], [fg; bg; shelf; given_up])
-let to_goals = function
-  | Element ("goals", [], [fg; bg; shelf; given_up]) ->
-    let to_glist = to_list to_goal in
-    let fg = to_list to_goal fg in
-    let bg = to_list (to_pair to_glist to_glist) bg in
-    let shelf = to_list to_goal shelf in
-    let given_up = to_list to_goal given_up in
-    { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up }
-  | _ -> raise Marshal_error
-
-let of_coq_info info =
-  let version = of_string info.coqtop_version in
-  let protocol = of_string info.protocol_version in
-  let release = of_string info.release_date in
-  let compile = of_string info.compile_date in
-  Element ("coq_info", [], [version; protocol; release; compile])
-let to_coq_info = function
-  | Element ("coq_info", [], [version; protocol; release; compile]) -> {
-      coqtop_version = to_string version;
-      protocol_version = to_string protocol;
-      release_date = to_string release;
-      compile_date = to_string compile; }
-  | _ -> raise Marshal_error
-
-let of_message_level = function
-  | Debug s -> constructor "message_level" "debug" [PCData s]
-  | Info -> constructor "message_level" "info" []
-  | Notice -> constructor "message_level" "notice" []
-  | Warning -> constructor "message_level" "warning" []
-  | Error -> constructor "message_level" "error" []
-let to_message_level = do_match "message_level" (fun s args -> match s with
-  | "debug" -> Debug (raw_string args)
-  | "info" -> Info
-  | "notice" -> Notice
-  | "warning" -> Warning
-  | "error" -> Error
-  | _ -> raise Marshal_error)
-
-let of_message msg =
-  let lvl = of_message_level msg.message_level in
-  let content = of_string msg.message_content in
-  Element ("message", [], [lvl; content])
-let to_message xml = match xml with
-  | Element ("message", [], [lvl; content]) -> {
-      message_level = to_message_level lvl;
-      message_content = to_string content }
-  | _ -> raise Marshal_error
-
-let is_message = function
-  | Element ("message", _, _) -> true
-  | _ -> false
-
 let of_loc loc =
   let start, stop = Loc.unloc loc in
   Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
-let to_loc xml = match xml with
+let to_loc xml =
+  match xml with
   | Element ("loc", l,[]) ->
       (try
         let start = massoc "start" l in
@@ -314,590 +114,3 @@ let to_loc xml = match xml with
       with Not_found | Invalid_argument _ -> raise Marshal_error)
   | _ -> raise Marshal_error
 
-let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
-  | "addedaxiom", _ -> AddedAxiom
-  | "processed", _ -> Processed
-  | "processinginmaster", _ -> ProcessingInMaster
-  | "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)
-  | "slavestatus", [ns] ->
-       let n, s = to_pair to_int to_string ns in
-       SlaveStatus(n,s)
-  | _ -> raise Marshal_error)
-let of_feedback_content = function
-  | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
-  | Processed -> constructor "feedback_content" "processed" []
-  | ProcessingInMaster -> constructor "feedback_content" "processinginmaster" []
-  | 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]
-  | SlaveStatus(n,s) ->
-      constructor "feedback_content" "slavestatus"
-        [of_pair of_int of_string (n,s)]
-
-let of_feedback msg =
-  let content = of_feedback_content msg.content in
-  let obj, id = of_edit_or_state_id msg.id in
-  Element ("feedback", obj, [id;content])
-let to_feedback xml = match xml with
-  | Element ("feedback", ["object","edit"], [id;content]) -> {
-      id = Interface.Edit(to_edit_id id);
-      content = to_feedback_content content }
-  | Element ("feedback", ["object","state"], [id;content]) -> { 
-      id = Interface.State(to_state_id id);
-      content = to_feedback_content content }
-  | _ -> raise Marshal_error
-
-end
-include Xml_marshalling
-
-(* Reification of basic types and type constructors, and functions
-   from to xml *)
-module ReifType : sig
-
-  type 'a val_t
-
-  val unit_t         : unit val_t
-  val string_t       : string val_t
-  val int_t          : int val_t
-  val bool_t         : bool val_t
-  
-  val option_t       : 'a val_t -> 'a option val_t
-  val list_t         : 'a val_t -> 'a list val_t
-  val pair_t         : 'a val_t -> 'b val_t -> ('a * 'b) val_t
-  val union_t        : 'a val_t -> 'b val_t -> ('a ,'b) union val_t
-
-  val goals_t        : goals val_t
-  val evar_t         : evar val_t
-  val state_t        : status val_t
-  val option_state_t : option_state val_t
-  val option_value_t : option_value val_t
-  val coq_info_t     : coq_info val_t
-  val coq_object_t   : 'a val_t -> 'a coq_object val_t
-  val state_id_t     : state_id val_t
-  val search_cst_t   : search_constraint val_t
-
-  val of_value_type : 'a val_t -> 'a -> xml
-  val to_value_type : 'a val_t -> xml -> 'a
-
-  val print         : 'a val_t -> 'a -> string
-
-  type value_type
-  val erase         : 'a val_t -> value_type
-  val print_type    : value_type -> string
-
-  val document_type_encoding : (xml -> string) -> unit
-
-end = struct
-
-  type value_type =
-    | Unit | String | Int | Bool
-
-    | Option of value_type
-    | List of value_type
-    | Pair of value_type * value_type
-    | Union of value_type * value_type
-    
-    | Goals | Evar | State | Option_state | Option_value | Coq_info
-    | Coq_object of value_type
-    | State_id
-    | Search_cst
-
-  type 'a val_t = value_type
-  
-  let erase (x : 'a val_t) : value_type = x
-
-  let unit_t         = Unit
-  let string_t       = String
-  let int_t          = Int
-  let bool_t         = Bool
-
-  let option_t x     = Option x
-  let list_t x       = List x
-  let pair_t x y     = Pair (x, y)
-  let union_t x y    = Union (x, y)
-
-  let goals_t        = Goals
-  let evar_t         = Evar
-  let state_t        = State
-  let option_state_t = Option_state
-  let option_value_t = Option_value
-  let coq_info_t     = Coq_info
-  let coq_object_t x = Coq_object x
-  let state_id_t     = State_id
-  let search_cst_t   = Search_cst
-
-  let of_value_type (ty : 'a val_t) : 'a -> xml =
-    let rec convert ty : 'a -> xml = match ty with
-      | Unit          -> Obj.magic of_unit
-      | Bool          -> Obj.magic of_bool
-      | String        -> Obj.magic of_string
-      | Int           -> Obj.magic of_int
-      | State         -> Obj.magic of_status
-      | Option_state  -> Obj.magic of_option_state
-      | Option_value  -> Obj.magic of_option_value
-      | Coq_info      -> Obj.magic of_coq_info
-      | Goals         -> Obj.magic of_goals
-      | Evar          -> Obj.magic of_evar
-      | List t        -> Obj.magic (of_list (convert t))
-      | Option t      -> Obj.magic (of_option (convert t))
-      | Coq_object t  -> Obj.magic (of_coq_object (convert t))
-      | Pair (t1,t2)  -> Obj.magic (of_pair (convert t1) (convert t2))
-      | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
-      | State_id      -> Obj.magic of_state_id
-      | Search_cst    -> Obj.magic of_search_cst
-    in
-      convert ty
-  
-  let to_value_type (ty : 'a val_t) : xml -> 'a =
-    let rec convert ty : xml -> 'a = match ty with
-      | Unit          -> Obj.magic to_unit
-      | Bool          -> Obj.magic to_bool
-      | String        -> Obj.magic to_string
-      | Int           -> Obj.magic to_int
-      | State         -> Obj.magic to_status
-      | Option_state  -> Obj.magic to_option_state
-      | Option_value  -> Obj.magic to_option_value
-      | Coq_info      -> Obj.magic to_coq_info
-      | Goals         -> Obj.magic to_goals
-      | Evar          -> Obj.magic to_evar
-      | List t        -> Obj.magic (to_list (convert t))
-      | Option t      -> Obj.magic (to_option (convert t))
-      | Coq_object t  -> Obj.magic (to_coq_object (convert t))
-      | Pair (t1,t2)  -> Obj.magic (to_pair (convert t1) (convert t2))
-      | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
-      | State_id      -> Obj.magic to_state_id
-      | Search_cst    -> Obj.magic to_search_cst
-    in
-      convert ty
-
-  let pr_unit () = ""
-  let pr_string s = Printf.sprintf "%S" s
-  let pr_int i = string_of_int i
-  let pr_bool b = Printf.sprintf "%B" b
-  let pr_goal (g : goals) =
-    if g.fg_goals = [] then
-      if g.bg_goals = [] then "Proof completed."
-      else
-        let rec pr_focus _ = function
-          | [] -> assert false
-          | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
-          | (lg, rg) :: l ->
-            Printf.sprintf "%i:%a"
-              (List.length lg + List.length rg) pr_focus l in
-        Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
-    else
-      let pr_menu s = s in
-      let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-        "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^
-            pr_menu goal ^ "]" in
-      String.concat " " (List.map pr_goal g.fg_goals)
-  let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
-  let pr_status (s : status) =
-    let path =
-      let l = String.concat "." s.status_path in
-      "path=" ^ l ^ ";" in
-    let name = match s.status_proofname with
-      | None -> "no proof;"
-      | Some n -> "proof = " ^ n ^ ";" in
-    "Status: " ^ path ^ name
-  let pr_coq_info (i : coq_info) = "FIXME"
-  let pr_option_value = function
-    | IntValue None -> "none"
-    | IntValue (Some i) -> string_of_int i
-    | StringValue s -> s
-    | BoolValue b -> if b then "true" else "false"
-  let pr_option_state (s : option_state) =
-    Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
-      s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
-  let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
-  let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
-  let pr_coq_object (o : 'a coq_object) = "FIXME"
-  let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")"
-  let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x
-
-  let pr_search_cst = function
-    | Name_Pattern s -> "Name_Pattern " ^ s
-    | Type_Pattern s -> "Type_Pattern " ^ s
-    | SubType_Pattern s -> "SubType_Pattern " ^ s
-    | In_Module s -> "In_Module " ^ String.concat "." s
-    | Include_Blacklist -> "Include_Blacklist"
-
-  let rec print = function
-  | Unit          -> Obj.magic pr_unit
-  | Bool          -> Obj.magic pr_bool
-  | String        -> Obj.magic pr_string
-  | Int           -> Obj.magic pr_int
-  | State         -> Obj.magic pr_status
-  | Option_state  -> Obj.magic pr_option_state
-  | Option_value  -> Obj.magic pr_option_value
-  | Search_cst    -> Obj.magic pr_search_cst
-  | Coq_info      -> Obj.magic pr_coq_info
-  | Goals         -> Obj.magic pr_goal
-  | Evar          -> Obj.magic pr_evar
-  | List t        -> Obj.magic (pr_list (print t))
-  | Option t      -> Obj.magic (pr_option (print t))
-  | Coq_object t  -> Obj.magic pr_coq_object
-  | Pair (t1,t2)  -> Obj.magic (pr_pair (print t1) (print t2))
-  | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2))
-  | State_id      -> Obj.magic pr_int
-
-  (* This is to break if a rename/refactoring makes the strings below outdated *)
-  type 'a exists = bool
-
-  let rec print_type = function
-  | Unit          -> "unit"
-  | Bool          -> "bool"
-  | String        -> "string"
-  | Int           -> "int"
-  | State         -> assert(true : status exists); "Interface.status"
-  | Option_state  -> assert(true : option_state exists); "Interface.option_state"
-  | Option_value  -> assert(true : option_value exists); "Interface.option_value"
-  | Search_cst    -> assert(true : search_constraint exists); "Interface.search_constraint"
-  | Coq_info      -> assert(true : coq_info exists); "Interface.coq_info"
-  | Goals         -> assert(true : goals exists); "Interface.goals"
-  | Evar          -> assert(true : evar exists); "Interface.evar"
-  | List t        -> Printf.sprintf "(%s list)" (print_type t)
-  | Option t      -> Printf.sprintf "(%s option)" (print_type t)
-  | Coq_object t  -> assert(true : 'a coq_object exists);
-                     Printf.sprintf "(%s Interface.coq_object)" (print_type t)
-  | Pair (t1,t2)  -> Printf.sprintf "(%s * %s)" (print_type t1) (print_type t2)
-  | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists);
-                     Printf.sprintf "((%s, %s) CSig.union)" (print_type t1) (print_type t2)
-  | State_id      -> assert(true : Stateid.t exists); "Stateid.t"
-
-  let document_type_encoding pr_xml =
-    Printf.printf "\n=== Data encoding by examples ===\n\n";
-    Printf.printf "%s:\n\n%s\n\n" (print_type Unit) (pr_xml (of_unit ()));
-    Printf.printf "%s:\n\n%s\n%s\n\n" (print_type Bool)
-      (pr_xml (of_bool true)) (pr_xml (of_bool false));
-    Printf.printf "%s:\n\n%s\n\n" (print_type String) (pr_xml (of_string "hello"));
-    Printf.printf "%s:\n\n%s\n\n" (print_type Int) (pr_xml (of_int 256));
-    Printf.printf "%s:\n\n%s\n\n" (print_type State_id) (pr_xml (of_state_id Stateid.initial));
-    Printf.printf "%s:\n\n%s\n\n" (print_type (List Int)) (pr_xml (of_list of_int [3;4;5]));
-    Printf.printf "%s:\n\n%s\n%s\n\n" (print_type (Option Int))
-      (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None));
-    Printf.printf "%s:\n\n%s\n\n" (print_type (Pair (Bool,Int)))
-      (pr_xml (of_pair of_bool of_int (false,3)));
-    Printf.printf "%s:\n\n%s\n\n" (print_type (Union (Bool,Int)))
-      (pr_xml (of_union of_bool of_int (Inl false)));
-    print_endline ("All other types are records represented by a node named like the OCaml\n"^
-                   "type which contains a flattened n-tuple.  We provide one example.\n");
-    Printf.printf "%s:\n\n%s\n\n" (print_type Option_state)
-      (pr_xml (of_option_state { opt_sync = true; opt_depr = false;
-        opt_name = "name1"; opt_value = IntValue (Some 37) }));
-
-end
-open ReifType
-
-(** Types reification, checked with explicit casts *)
-let add_sty_t : add_sty val_t = 
-  pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t)
-let edit_at_sty_t : edit_at_sty val_t = state_id_t
-let query_sty_t : query_sty val_t = pair_t string_t state_id_t
-let goals_sty_t : goals_sty val_t = unit_t
-let evars_sty_t : evars_sty val_t = unit_t
-let hints_sty_t : hints_sty val_t = unit_t
-let status_sty_t : status_sty val_t = bool_t
-let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t)
-let get_options_sty_t : get_options_sty val_t = unit_t
-let set_options_sty_t : set_options_sty val_t =
-  list_t (pair_t (list_t string_t) option_value_t)
-let mkcases_sty_t : mkcases_sty val_t = string_t
-let quit_sty_t : quit_sty val_t = unit_t
-let about_sty_t : about_sty val_t = unit_t
-let init_sty_t : init_sty val_t = option_t string_t
-let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
-let stop_worker_sty_t : stop_worker_sty val_t = int_t
-
-let add_rty_t : add_rty val_t =
-  pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
-let edit_at_rty_t : edit_at_rty val_t =
-  union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t))
-let query_rty_t : query_rty val_t = string_t
-let goals_rty_t : goals_rty val_t = option_t goals_t
-let evars_rty_t : evars_rty val_t = option_t (list_t evar_t)
-let hints_rty_t : hints_rty val_t =
-  let hint = list_t (pair_t string_t string_t) in
-  option_t (pair_t (list_t hint) hint)
-let status_rty_t : status_rty val_t = state_t
-let search_rty_t : search_rty val_t = list_t (coq_object_t string_t)
-let get_options_rty_t : get_options_rty val_t =
-  list_t (pair_t (list_t string_t) option_state_t) 
-let set_options_rty_t : set_options_rty val_t = unit_t
-let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t)
-let quit_rty_t : quit_rty val_t = unit_t
-let about_rty_t : about_rty val_t = coq_info_t
-let init_rty_t : init_rty val_t = state_id_t
-let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t)
-let stop_worker_rty_t : stop_worker_rty val_t = unit_t
-
-let ($) x = erase x
-let calls = [|  
-  "Add",        ($)add_sty_t,         ($)add_rty_t;
-  "Edit_at",    ($)edit_at_sty_t,     ($)edit_at_rty_t;
-  "Query",      ($)query_sty_t,       ($)query_rty_t;
-  "Goal",       ($)goals_sty_t,       ($)goals_rty_t;
-  "Evars",      ($)evars_sty_t,       ($)evars_rty_t;
-  "Hints",      ($)hints_sty_t,       ($)hints_rty_t;
-  "Status",     ($)status_sty_t,      ($)status_rty_t;
-  "Search",     ($)search_sty_t,      ($)search_rty_t;
-  "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t;
-  "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t;
-  "MkCases",    ($)mkcases_sty_t,     ($)mkcases_rty_t;
-  "Quit",       ($)quit_sty_t,        ($)quit_rty_t;
-  "About",      ($)about_sty_t,       ($)about_rty_t;
-  "Init",       ($)init_sty_t,        ($)init_rty_t;
-  "Interp",     ($)interp_sty_t,      ($)interp_rty_t;
-  "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t;
-|]
-
-type 'a call =
-  | Add        of add_sty
-  | Edit_at    of edit_at_sty
-  | Query      of query_sty
-  | Goal       of goals_sty
-  | Evars      of evars_sty
-  | Hints      of hints_sty
-  | Status     of status_sty
-  | Search     of search_sty
-  | GetOptions of get_options_sty
-  | SetOptions of set_options_sty
-  | MkCases    of mkcases_sty
-  | Quit       of quit_sty
-  | About      of about_sty
-  | Init       of init_sty
-  | StopWorker of stop_worker_sty
-  (* retrocompatibility *)
-  | Interp     of interp_sty
-
-let id_of_call = function
-  | Add _        -> 0
-  | Edit_at _    -> 1
-  | Query _      -> 2
-  | Goal _       -> 3
-  | Evars _      -> 4
-  | Hints _      -> 5
-  | Status _     -> 6
-  | Search _     -> 7
-  | GetOptions _ -> 8
-  | SetOptions _ -> 9
-  | MkCases _    -> 10
-  | Quit _       -> 11
-  | About _      -> 12
-  | Init _       -> 13
-  | Interp _     -> 14
-  | StopWorker _ -> 15
-
-let str_of_call c = pi1 calls.(id_of_call c)
-
-type unknown
-
-(** We use phantom types and GADT to protect ourselves against wild casts *)
-let add x         : add_rty call         = Add x
-let edit_at x     : edit_at_rty call     = Edit_at x
-let query x       : query_rty call       = Query x
-let goals x       : goals_rty call       = Goal x
-let evars x       : evars_rty call       = Evars x
-let hints x       : hints_rty call       = Hints x
-let status x      : status_rty call      = Status x
-let get_options x : get_options_rty call = GetOptions x
-let set_options x : set_options_rty call = SetOptions x
-let mkcases x     : mkcases_rty call     = MkCases x
-let search x      : search_rty call      = Search x
-let quit x        : quit_rty call        = Quit x
-let init x        : init_rty call        = Init x
-let interp x      : interp_rty call      = Interp x
-let stop_worker x : stop_worker_rty call = StopWorker x
-
-let abstract_eval_call handler (c : 'a call) : 'a value =
-  let mkGood x : 'a value = Good (Obj.magic x) in
-  try
-    match c with
-    | Add x        -> mkGood (handler.add x)
-    | Edit_at x    -> mkGood (handler.edit_at x)
-    | Query x      -> mkGood (handler.query x)
-    | Goal x       -> mkGood (handler.goals x)
-    | Evars x      -> mkGood (handler.evars x)
-    | Hints x      -> mkGood (handler.hints x)
-    | Status x     -> mkGood (handler.status x)
-    | Search x     -> mkGood (handler.search x)
-    | GetOptions x -> mkGood (handler.get_options x)
-    | SetOptions x -> mkGood (handler.set_options x)
-    | MkCases x    -> mkGood (handler.mkcases x)
-    | Quit x       -> mkGood (handler.quit x)
-    | About x      -> mkGood (handler.about x)
-    | Init x       -> mkGood (handler.init x)
-    | Interp x     -> mkGood (handler.interp x)
-    | StopWorker x -> mkGood (handler.stop_worker x)
-  with any ->
-    Fail (handler.handle_exn any)
-
-(** brain dead code, edit if protocol messages are added/removed *)
-let of_answer (q : 'a call) (v : 'a value) : xml = match q with
-  | Add _        -> of_value (of_value_type add_rty_t        ) (Obj.magic v)
-  | Edit_at _    -> of_value (of_value_type edit_at_rty_t    ) (Obj.magic v)
-  | Query _      -> of_value (of_value_type query_rty_t      ) (Obj.magic v)
-  | Goal _       -> of_value (of_value_type goals_rty_t      ) (Obj.magic v)
-  | Evars _      -> of_value (of_value_type evars_rty_t      ) (Obj.magic v)
-  | Hints _      -> of_value (of_value_type hints_rty_t      ) (Obj.magic v)
-  | Status _     -> of_value (of_value_type status_rty_t     ) (Obj.magic v)
-  | Search _     -> of_value (of_value_type search_rty_t     ) (Obj.magic v)
-  | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v)
-  | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v)
-  | MkCases _    -> of_value (of_value_type mkcases_rty_t    ) (Obj.magic v)
-  | Quit _       -> of_value (of_value_type quit_rty_t       ) (Obj.magic v)
-  | About _      -> of_value (of_value_type about_rty_t      ) (Obj.magic v)
-  | Init _       -> of_value (of_value_type init_rty_t       ) (Obj.magic v)
-  | Interp _     -> of_value (of_value_type interp_rty_t     ) (Obj.magic v)
-  | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v)
-
-let to_answer (q : 'a call) (x : xml) : 'a value = match q with
-  | Add _        -> Obj.magic (to_value (to_value_type add_rty_t        ) x)
-  | Edit_at _    -> Obj.magic (to_value (to_value_type edit_at_rty_t    ) x)
-  | Query _      -> Obj.magic (to_value (to_value_type query_rty_t      ) x)
-  | Goal _       -> Obj.magic (to_value (to_value_type goals_rty_t      ) x)
-  | Evars _      -> Obj.magic (to_value (to_value_type evars_rty_t      ) x)
-  | Hints _      -> Obj.magic (to_value (to_value_type hints_rty_t      ) x)
-  | Status _     -> Obj.magic (to_value (to_value_type status_rty_t     ) x)
-  | Search _     -> Obj.magic (to_value (to_value_type search_rty_t     ) x)
-  | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x)
-  | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x)
-  | MkCases _    -> Obj.magic (to_value (to_value_type mkcases_rty_t    ) x)
-  | Quit _       -> Obj.magic (to_value (to_value_type quit_rty_t       ) x)
-  | About _      -> Obj.magic (to_value (to_value_type about_rty_t      ) x)
-  | Init _       -> Obj.magic (to_value (to_value_type init_rty_t       ) x)
-  | Interp _     -> Obj.magic (to_value (to_value_type interp_rty_t     ) x)
-  | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x)
-
-let of_call (q : 'a call) : xml =
-  let mkCall x = constructor "call" (str_of_call q) [x] in
-  match q with
-  | Add x        -> mkCall (of_value_type add_sty_t         x) 
-  | Edit_at x    -> mkCall (of_value_type edit_at_sty_t     x) 
-  | Query x      -> mkCall (of_value_type query_sty_t       x) 
-  | Goal x       -> mkCall (of_value_type goals_sty_t       x) 
-  | Evars x      -> mkCall (of_value_type evars_sty_t       x) 
-  | Hints x      -> mkCall (of_value_type hints_sty_t       x) 
-  | Status x     -> mkCall (of_value_type status_sty_t      x) 
-  | Search x     -> mkCall (of_value_type search_sty_t      x) 
-  | GetOptions x -> mkCall (of_value_type get_options_sty_t x) 
-  | SetOptions x -> mkCall (of_value_type set_options_sty_t x) 
-  | MkCases x    -> mkCall (of_value_type mkcases_sty_t     x) 
-  | Quit x       -> mkCall (of_value_type quit_sty_t        x) 
-  | About x      -> mkCall (of_value_type about_sty_t       x) 
-  | Init x       -> mkCall (of_value_type init_sty_t        x)
-  | Interp x     -> mkCall (of_value_type interp_sty_t      x)
-  | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x)
-
-let to_call : xml -> unknown call =
-  do_match "call" (fun s a ->
-    let mkCallArg vt a = to_value_type vt (singleton a) in
-    match s with
-    | "Add"        -> Add        (mkCallArg add_sty_t         a)
-    | "Edit_at"    -> Edit_at    (mkCallArg edit_at_sty_t     a)
-    | "Query"      -> Query      (mkCallArg query_sty_t       a)
-    | "Goal"       -> Goal       (mkCallArg goals_sty_t       a)
-    | "Evars"      -> Evars      (mkCallArg evars_sty_t       a)
-    | "Hints"      -> Hints      (mkCallArg hints_sty_t       a)
-    | "Status"     -> Status     (mkCallArg status_sty_t      a)
-    | "Search"     -> Search     (mkCallArg search_sty_t      a)
-    | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a)
-    | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a)
-    | "MkCases"    -> MkCases    (mkCallArg mkcases_sty_t     a)
-    | "Quit"       -> Quit       (mkCallArg quit_sty_t        a)
-    | "About"      -> About      (mkCallArg about_sty_t       a)
-    | "Init"       -> Init       (mkCallArg init_sty_t        a)
-    | "Interp"     -> Interp     (mkCallArg interp_sty_t      a)
-    | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a)
-    | _ -> raise Marshal_error)
-
-(** misc *)
-
-let is_feedback = function
-  | Element ("feedback", _, _) -> true
-  | _ -> false
-
-(** Debug printing *)
-
-let pr_value_gen pr = function
-  | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]"
-  | Fail (id,Some(i,j),str) ->
-      "FAIL "^Stateid.to_string id^
-        " ("^string_of_int i^","^string_of_int j^")["^str^"]"
-let pr_value v = pr_value_gen (fun _ -> "FIXME") v
-let pr_full_value call value = match call with
-  | Add _        -> pr_value_gen (print add_rty_t        ) (Obj.magic value) 
-  | Edit_at _    -> pr_value_gen (print edit_at_rty_t    ) (Obj.magic value) 
-  | Query _      -> pr_value_gen (print query_rty_t      ) (Obj.magic value) 
-  | Goal _       -> pr_value_gen (print goals_rty_t      ) (Obj.magic value) 
-  | Evars _      -> pr_value_gen (print evars_rty_t      ) (Obj.magic value) 
-  | Hints _      -> pr_value_gen (print hints_rty_t      ) (Obj.magic value) 
-  | Status _     -> pr_value_gen (print status_rty_t     ) (Obj.magic value) 
-  | Search _     -> pr_value_gen (print search_rty_t     ) (Obj.magic value) 
-  | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) 
-  | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) 
-  | MkCases _    -> pr_value_gen (print mkcases_rty_t    ) (Obj.magic value) 
-  | Quit _       -> pr_value_gen (print quit_rty_t       ) (Obj.magic value) 
-  | About _      -> pr_value_gen (print about_rty_t      ) (Obj.magic value) 
-  | Init _       -> pr_value_gen (print init_rty_t       ) (Obj.magic value)
-  | Interp _     -> pr_value_gen (print interp_rty_t     ) (Obj.magic value)
-  | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value)
-let pr_call call = match call with
-  | Add x        -> str_of_call call ^ " " ^ print add_sty_t         x
-  | Edit_at x    -> str_of_call call ^ " " ^ print edit_at_sty_t     x
-  | Query x      -> str_of_call call ^ " " ^ print query_sty_t       x
-  | Goal x       -> str_of_call call ^ " " ^ print goals_sty_t       x
-  | Evars x      -> str_of_call call ^ " " ^ print evars_sty_t       x
-  | Hints x      -> str_of_call call ^ " " ^ print hints_sty_t       x
-  | Status x     -> str_of_call call ^ " " ^ print status_sty_t      x
-  | Search x     -> str_of_call call ^ " " ^ print search_sty_t      x
-  | GetOptions x -> str_of_call call ^ " " ^ print get_options_sty_t x
-  | SetOptions x -> str_of_call call ^ " " ^ print set_options_sty_t x
-  | MkCases x    -> str_of_call call ^ " " ^ print mkcases_sty_t     x
-  | Quit x       -> str_of_call call ^ " " ^ print quit_sty_t        x
-  | About x      -> str_of_call call ^ " " ^ print about_sty_t       x
-  | Init x       -> str_of_call call ^ " " ^ print init_sty_t        x
-  | Interp x     -> str_of_call call ^ " " ^ print interp_sty_t      x
-  | StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x
-
-let document to_string_fmt =
-  Printf.printf "=== Available calls ===\n\n";
-  Array.iter (fun (cname, csty, crty) ->
-      Printf.printf "%12s :  %s\n %14s %s\n"
-        ("\""^cname^"\"") (print_type csty) "->" (print_type crty))
-    calls;
-  Printf.printf "\n=== Calls XML encoding ===\n\n";
-  Printf.printf "A call \"C\" carrying input a is encoded as:\n\n%s\n\n"
-    (to_string_fmt (constructor "call" "C" [PCData "a"]));
-  Printf.printf "A response carrying output b can either be:\n\n%s\n\n"
-    (to_string_fmt (of_value (fun _ -> PCData "b") (Good ())));
-  Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n"
-    (to_string_fmt (of_value (fun _ -> PCData "b")
-      (Fail (Stateid.initial,Some (15,34),"error message"))));
-  document_type_encoding to_string_fmt
-
-(* vim: set foldmethod=marker: *)
diff --git a/lib/serialize.mli b/lib/serialize.mli
index b8bb1a33a..55c5ff041 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -6,61 +6,32 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** * Applicative part of the interface of CoqIde calls to Coq *)
-
-open Interface
 open Xml_datatype
 
-type 'a call
-
-type unknown
-
-val add         : add_sty         -> add_rty call
-val edit_at     : edit_at_sty     -> edit_at_rty call
-val query       : query_sty       -> query_rty call
-val goals       : goals_sty       -> goals_rty call
-val hints       : hints_sty       -> hints_rty call
-val status      : status_sty      -> status_rty call
-val mkcases     : mkcases_sty     -> mkcases_rty call
-val evars       : evars_sty       -> evars_rty call
-val search      : search_sty      -> search_rty call
-val get_options : get_options_sty -> get_options_rty call
-val set_options : set_options_sty -> set_options_rty call
-val quit        : quit_sty        -> quit_rty call
-val init        : init_sty        -> init_rty call
-val stop_worker : stop_worker_sty -> stop_worker_rty call
-(* retrocompatibility *)
-val interp      : interp_sty      -> interp_rty call
-
-val abstract_eval_call : handler -> 'a call -> 'a value
-
-(** * Protocol version *)
-
-val protocol_version : string
-
-(** * XML data marshalling *)
-
 exception Marshal_error
 
-val of_call : 'a call -> xml
-val to_call : xml -> unknown call
-
-val of_message : message -> xml
-val to_message : xml -> message
-val is_message : xml -> bool
-
-val of_feedback : feedback -> xml
-val to_feedback : xml -> feedback
-val is_feedback : xml -> bool
-
-val of_answer : 'a call -> 'a value -> xml
-val to_answer : 'a call -> xml -> 'a value
-
-(* Prints the documentation of this module *)
-val document : (xml -> string) -> unit
-
-(** * Debug printing *)
-
-val pr_call : 'a call -> string
-val pr_value : 'a value -> string
-val pr_full_value : 'a call -> 'a value -> string
+val massoc: string -> (string * string) list -> string
+val constructor: string -> string -> xml list -> xml
+val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b
+val singleton: 'a list -> 'a
+val raw_string: xml list -> string
+val of_unit: unit -> xml
+val to_unit: xml -> unit
+val of_bool: bool -> xml
+val to_bool: xml -> bool
+val of_list: ('a -> xml) -> 'a list -> xml
+val to_list: (xml -> 'a) -> xml -> 'a list
+val of_option: ('a -> xml) -> 'a option -> xml
+val to_option: (xml -> 'a) -> xml -> 'a option
+val of_string: string -> xml
+val to_string: xml -> string
+val of_int: int -> xml
+val to_int: xml -> int
+val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml
+val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b
+val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml
+val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union
+val of_edit_id: int -> xml
+val to_edit_id: xml -> int
+val of_loc : Loc.t -> xml
+val to_loc : xml -> Loc.t
diff --git a/library/goptions.ml b/library/goptions.ml
index 8402abd34..c348548e7 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -15,9 +15,19 @@ open Libobject
 open Libnames
 open Mod_subst
 
-open Interface
-
-type option_name = Interface.option_name
+type option_name = string list
+type option_value =
+  | BoolValue   of bool
+  | IntValue    of int option
+  | StringValue of string
+
+(** Summary of an option status *)
+type option_state = {
+  opt_sync  : bool;
+  opt_depr  : bool;
+  opt_name  : string;
+  opt_value : option_value;
+}
 
 (****************************************************************************)
 (* 0- Common things                                                         *)
@@ -354,7 +364,6 @@ let print_option_value key =
     | _ ->
 	msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s))
 
-
 let get_tables () =
   let tables = !value_tab in
   let fold key (name, depr, (sync,read,_,_,_)) accu =
diff --git a/library/goptions.mli b/library/goptions.mli
index 6251b8d2d..f249a97be 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -47,7 +47,7 @@ open Pp
 open Libnames
 open Mod_subst
 
-type option_name = Interface.option_name
+type option_name = string list
 
 (** {6 Tables. } *)
 
@@ -161,7 +161,20 @@ val set_string_option_value : option_name -> string -> unit
 
 val print_option_value : option_name -> unit
 
-val get_tables : unit -> Interface.option_state OptionMap.t
+type option_value =
+  | BoolValue   of bool
+  | IntValue    of int option
+  | StringValue of string
+
+(** Summary of an option status *)
+type option_state = {
+  opt_sync  : bool;
+  opt_depr  : bool;
+  opt_name  : string;
+  opt_value : option_value;
+}
+
+val get_tables : unit -> option_state OptionMap.t
 val print_tables : unit -> std_ppcmds
 
 val error_undeclared_key : option_name -> 'a
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index c40000811..5d2babaca 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -323,7 +323,7 @@ let standard_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit hook ();
-      Pp.feedback Interface.AddedAxiom
+      Pp.feedback Feedback.AddedAxiom
   | Proved (is_opaque,idopt,proof) ->
       let proof = get_proof proof compute_guard hook is_opaque in
       begin match idopt with
@@ -337,7 +337,7 @@ let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
   | Admitted ->
       admit (hook Evd.empty_evar_universe_context) ();
-      Pp.feedback Interface.AddedAxiom
+      Pp.feedback Feedback.AddedAxiom
   | Proved (is_opaque,idopt,proof) ->
       let proof = get_proof proof compute_guard 
 	(hook proof.Proof_global.universes) is_opaque in
diff --git a/stm/stm.ml b/stm/stm.ml
index 85c3838dc..b53c9fcf8 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -51,7 +51,7 @@ let vernac_interp ?proof id { verbose; loc; expr } =
   if internal_command expr then begin
     prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
   end else begin
-    Pp.set_id_for_feedback (Interface.State id);
+    Pp.set_id_for_feedback (Feedback.State id);
     Aux_file.record_in_aux_set_at loc;
     prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
     let interp = Hook.get f_interp in
@@ -63,7 +63,7 @@ let vernac_interp ?proof id { verbose; loc; expr } =
 
 (* Wrapper for Vernac.parse_sentence to set the feedback id *)
 let vernac_parse eid s =
-  set_id_for_feedback (Interface.Edit eid);
+  set_id_for_feedback (Feedback.Edit eid);
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   Flags.with_option Flags.we_are_parsing (fun () ->
     match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
@@ -570,7 +570,7 @@ end = struct
     | None ->
         let loc = Option.default Loc.ghost (Loc.get_loc e) in
         let msg = string_of_ppcmds (print e) in
-        Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg));
+        Pp.feedback ~state_id:id (Feedback.ErrorMsg (loc, msg));
         Stateid.add (Hook.get f_process_error e) ?valid id
 
   let define ?(redefine=false) ?(cache=`No) f id =
@@ -585,7 +585,7 @@ end = struct
       else if cache = `Shallow then freeze `Shallow id;
       prerr_endline ("setting cur id to "^str_id);
       cur_id := id;
-      feedback ~state_id:id Interface.Processed;
+      feedback ~state_id:id Feedback.Processed;
       VCS.reached id true;
       if Proof_global.there_are_pending_proofs () then
         VCS.goals id (Proof_global.get_open_goals ());
@@ -687,7 +687,7 @@ end = struct
     | RespError of (* err, safe, msg, safe_states *)
         Stateid.t * Stateid.t * std_ppcmds *
           (Stateid.t * State.frozen_state) list
-    | RespFeedback of Interface.feedback
+    | RespFeedback of Feedback.feedback
     | RespGetCounterNewUnivLevel
 
   type more_data =
@@ -825,8 +825,6 @@ end = struct
         with Not_found -> 0.0 in
       s,max (time1 +. time2) 0.0001,i) 0 l
 
-  open Interface
-
   exception MarshalError of string
 
   let marshal_to_channel oc data =
@@ -900,7 +898,7 @@ end = struct
     else 
       let f, assign = Future.create_delegate (State.exn_on id ~valid) in
       let uuid = Future.uuid f in
-      Pp.feedback (Interface.InProgress 1);
+      Pp.feedback (Feedback.InProgress 1);
       TQueue.push queue (TaskBuildProof
         (exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
       f, cancel_switch
@@ -920,7 +918,7 @@ end = struct
           match !Flags.async_proofs_mode with
           | Flags.APonParallel n -> n
           | _ -> assert false in
-    Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s))
+    Pp.feedback ~state_id:Stateid.initial (Feedback.SlaveStatus(id, s))
 
   let rec manage_slave ~cancel:cancel_user_req id_slave respawn =
     let ic, oc, proc =
@@ -962,7 +960,7 @@ end = struct
               RespBuiltProof(pl, time)->
                 assign (`Val pl);
                 (* We restart the slave, to avoid memory leaks.  We could just
-                   Pp.feedback (Interface.InProgress ~-1) *)
+                   Pp.feedback (Feedback.InProgress ~-1) *)
                 record_pb_time s loc time;
                 last_task := None;
                 raise KillRespawn
@@ -972,7 +970,7 @@ end = struct
                 assign (`Exn e);
                 List.iter (fun (id,s) -> State.assign id s) valid_states;
                 (* We restart the slave, to avoid memory leaks.  We could just
-                   Pp.feedback (Interface.InProgress ~-1) *)
+                   Pp.feedback (Feedback.InProgress ~-1) *)
                 last_task := None;
                 raise KillRespawn
                 (* marshal_more_data oc (MoreDataLocalUniv *)
@@ -982,7 +980,7 @@ end = struct
                 marshal_more_data oc (MoreDataUnivLevel
                   (CList.init 10 (fun _ -> Universes.new_univ_level (Global.current_dirpath ()))));
                 loop ()
-            | _, RespFeedback {id = State state_id; content = msg} ->
+            | _, RespFeedback {Feedback.id = Feedback.State state_id; content = msg} ->
                 Pp.feedback ~state_id msg;
                 loop ()
             | _, RespFeedback _ -> assert false (* Parsing in master process *)
@@ -990,7 +988,7 @@ end = struct
             loop ()
         with
         | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *)
-            Pp.feedback (Interface.InProgress ~-1);
+            Pp.feedback (Feedback.InProgress ~-1);
             prerr_endline ("Task expired: " ^ pr_task task)
         | (Sys_error _ | Invalid_argument _ | End_of_file | KillRespawn) as e ->
             raise e (* we pass the exception to the external handler *)
@@ -1000,7 +998,7 @@ end = struct
               "Falling back to local, lazy, evaluation."));
             let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
             assign(`Comp(build_proof_here exn_info loc stop));
-            Pp.feedback (Interface.InProgress ~-1)
+            Pp.feedback (Feedback.InProgress ~-1)
         | MarshalError s ->
             pr_err ("Fatal marshal error: " ^ s);
             flush_all (); exit 1
@@ -1011,11 +1009,11 @@ end = struct
       done
     with
     | KillRespawn ->
-        Pp.feedback (Interface.InProgress ~-1);
+        Pp.feedback (Feedback.InProgress ~-1);
         Worker.kill proc; ignore(Worker.wait proc);
         manage_slave ~cancel:cancel_user_req id_slave respawn
     | Sys_error _ | Invalid_argument _ | End_of_file when !task_expired ->
-        Pp.feedback (Interface.InProgress ~-1);
+        Pp.feedback (Feedback.InProgress ~-1);
         ignore(Worker.wait proc);
         manage_slave ~cancel:cancel_user_req id_slave respawn
     | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled ->
@@ -1025,8 +1023,8 @@ end = struct
           let s = "Worker cancelled by the user" in
           let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in
           assign (`Exn e);
-          Pp.feedback ~state_id:start (Interface.ErrorMsg (Loc.ghost, s));
-          Pp.feedback (Interface.InProgress ~-1);
+          Pp.feedback ~state_id:start (Feedback.ErrorMsg (Loc.ghost, s));
+          Pp.feedback (Feedback.InProgress ~-1);
         ) !last_task;
         Worker.kill proc; ignore(Worker.wait proc);
         manage_slave ~cancel:cancel_user_req id_slave respawn
@@ -1037,7 +1035,7 @@ end = struct
           msg_warning(strbrk "Falling back to local, lazy, evaluation.");
           let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
           assign(`Comp(build_proof_here exn_info loc stop));
-          Pp.feedback (Interface.InProgress ~-1);
+          Pp.feedback (Feedback.InProgress ~-1);
         ) !last_task;
         Worker.kill proc; ignore(Worker.wait proc);
         manage_slave ~cancel:cancel_user_req id_slave respawn
@@ -1252,7 +1250,7 @@ let known_state ?(redefine_qed=false) ~cache id =
     prerr_endline ("reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached id then begin
       State.install_cached id;
-      feedback ~state_id:id Interface.Processed;
+      feedback ~state_id:id Feedback.Processed;
       prerr_endline ("reached (cache)")
     end else
     let step, cache_step =
@@ -1292,7 +1290,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                       Proof_global.close_future_proof ~feedback_id:id fp in
                     reach view.next;
                     vernac_interp id ~proof x;
-                    feedback ~state_id:id Interface.Incomplete
+                    feedback ~state_id:id Feedback.Incomplete
                 | VtDrop, _, _ ->
                     reach view.next;
                     Option.iter (vernac_interp start) proof_using_ast;
@@ -1347,7 +1345,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache
     in
     if !Flags.async_proofs_mode = Flags.APonParallel 0 then
-      Pp.feedback ~state_id:id Interface.ProcessingInMaster;
+      Pp.feedback ~state_id:id Feedback.ProcessingInMaster;
     State.define ~cache:cache_step ~redefine:redefine_qed step id;
     prerr_endline ("reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
diff --git a/stm/stm.mli b/stm/stm.mli
index a58100b5a..fd306425c 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -7,8 +7,8 @@
 (************************************************************************)
 
 open Vernacexpr
-open Interface
 open Names
+open Feedback
 
 (** state-transaction-machine interface *)
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 068dfb2ee..df114d059 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -20,23 +20,23 @@ type coqtop = {
 let logger level content = prerr_endline content
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
-  if print then prerr_endline (Serialize.pr_call call);
-  let xml_query = Serialize.of_call call in
+  if print then prerr_endline (Xmlprotocol.pr_call call);
+  let xml_query = Xmlprotocol.of_call call in
   Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
-    if Serialize.is_message xml then
-      let message = Serialize.to_message xml in
-      let level = message.Interface.message_level in
-      let content = message.Interface.message_content in
+    if Pp.is_message xml then
+      let message = Pp.to_message xml in
+      let level = message.Pp.message_level in
+      let content = message.Pp.message_content in
       logger level content;
       loop ()
-    else if Serialize.is_feedback xml then
+    else if Feedback.is_feedback xml then
       loop ()
-    else (Serialize.to_answer call xml)
+    else (Xmlprotocol.to_answer call xml)
   in
   let res = loop () in
-  if print then prerr_endline (Serialize.pr_full_value call res);
+  if print then prerr_endline (Xmlprotocol.pr_full_value call res);
   match res with
   | Interface.Fail (_,_,s) when fail -> error s
   | Interface.Fail (_,_,s) as x -> prerr_endline s; x
@@ -224,7 +224,7 @@ module GUILogic = struct
         let to_id, need_unfocus =
           get_id_pred (fun id _ -> Stateid.equal id safe_id) in
         after_edit_at (to_id, need_unfocus)
-          (base_eval_call (Serialize.edit_at to_id) coq)
+          (base_eval_call (Xmlprotocol.edit_at to_id) coq)
     | Interface.Good _ -> error "The command was expected to fail but did not"
 
 end
@@ -233,7 +233,7 @@ open GUILogic
 
 let eval_print l coq =
   let open Parser in
-  let open Serialize in
+  let open Xmlprotocol in
   (* prerr_endline ("Interpreting: " ^ print_toklist l); *)
   match l with
   | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] ->
@@ -311,15 +311,15 @@ let main =
     Xml_parser.check_eof ip false;
     { xml_printer = op; xml_parser = ip } in
   let init () =
-    match base_eval_call ~print:false (Serialize.init None) coq with
+    match base_eval_call ~print:false (Xmlprotocol.init None) coq with
     | Interface.Good id ->
         let dir = Filename.dirname input_file in
         let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in
         let eid, tip = add_sentence ~name:"initial" phrase in
-        after_add (base_eval_call (Serialize.add ((phrase,eid),(tip,true))) coq)
+        after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq)
     | Interface.Fail _ -> error "init call failed" in
   let finish () =
-    match base_eval_call (Serialize.status true) coq with
+    match base_eval_call (Xmlprotocol.status true) coq with
     | Interface.Good _ -> exit 0
     | Interface.Fail (_,_,s) -> error s in
   (* The main loop *)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 45aa980b7..2f778be36 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -95,7 +95,7 @@ let init_load_path () =
     (* main loops *)
     Mltop.add_ml_dir (coqlib/"toploop");
     if Coq_config.local then Mltop.add_ml_dir (coqlib/"stm");
-    if Coq_config.local then Mltop.add_ml_dir (coqlib/"idetop");
+    if Coq_config.local then Mltop.add_ml_dir (coqlib/"ide");
     (* then standard library *)
     add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0523ffd44..d64e3d979 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -389,8 +389,6 @@ let parse_args arglist =
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
-    |"--help-XML-protocol" ->
-        Serialize.document Xml_printer.to_string_fmt; exit 0
     |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
     |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 37403504d..016b9f22b 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -217,26 +217,39 @@ let search_about items mods =
   let () = generic_search iter in
   format_display !ans
 
+type search_constraint =
+  | Name_Pattern of string
+  | Type_Pattern of string
+  | SubType_Pattern of string
+  | In_Module of string list
+  | Include_Blacklist
+
+type 'a coq_object = {
+  coq_object_prefix : string list;
+  coq_object_qualid : string list;
+  coq_object_object : 'a;
+}
+
 let interface_search flags =
   let env = Global.env () in
   let rec extract_flags name tpe subtpe mods blacklist = function
   | [] -> (name, tpe, subtpe, mods, blacklist)
-  | (Interface.Name_Pattern s, b) :: l ->
+  | (Name_Pattern s, b) :: l ->
     let regexp =
       try Str.regexp s
       with e when Errors.noncritical e ->
         Errors.error ("Invalid regexp: " ^ s)
     in
     extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
-  | (Interface.Type_Pattern s, b) :: l ->
+  | (Type_Pattern s, b) :: l ->
     let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
     let (_, pat) = Constrintern.intern_constr_pattern env constr in
     extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
-  | (Interface.SubType_Pattern s, b) :: l ->
+  | (SubType_Pattern s, b) :: l ->
     let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
     let (_, pat) = Constrintern.intern_constr_pattern env constr in
     extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
-  | (Interface.In_Module m, b) :: l ->
+  | (In_Module m, b) :: l ->
     let path = String.concat "." m in
     let m = Pcoq.parse_string Pcoq.Constr.global path in
     let (_, qid) = Libnames.qualid_of_reference m in
@@ -246,7 +259,7 @@ let interface_search flags =
         Errors.error ("Module " ^ path ^ " not found.")
     in
     extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
-  | (Interface.Include_Blacklist, b) :: l ->
+  | (Include_Blacklist, b) :: l ->
     extract_flags name tpe subtpe mods b l
   in
   let (name, tpe, subtpe, mods, blacklist) =
@@ -295,9 +308,9 @@ let interface_search flags =
     in
     let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in
     let answer = {
-      Interface.coq_object_prefix = prefix;
-      Interface.coq_object_qualid = qualid;
-      Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr);
+      coq_object_prefix = prefix;
+      coq_object_qualid = qualid;
+      coq_object_object = string_of_ppcmds (pr_lconstr_env env constr);
     } in
     ans := answer :: !ans;
   in
diff --git a/toplevel/search.mli b/toplevel/search.mli
index c06a64be1..a69a8db79 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -40,8 +40,27 @@ val search_rewrite : constr_pattern -> DirPath.t list * bool -> std_ppcmds
 val search_pattern : constr_pattern -> DirPath.t list * bool -> std_ppcmds
 val search_about   : (bool * glob_search_about_item) list ->
   DirPath.t list * bool -> std_ppcmds
-val interface_search : (Interface.search_constraint * bool) list ->
-  string Interface.coq_object list
+
+type search_constraint =
+  (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
+  | Name_Pattern of string
+  (** Whether the object type satisfies a pattern *)
+  | Type_Pattern of string
+  (** Whether some subtype of object type satisfies a pattern *)
+  | SubType_Pattern of string
+  (** Whether the object pertains to a module *)
+  | In_Module of string list
+  (** Bypass the Search blacklist *)
+  | Include_Blacklist
+
+type 'a coq_object = {
+  coq_object_prefix : string list;
+  coq_object_qualid : string list;
+  coq_object_object : 'a;
+}
+
+val interface_search : (search_constraint * bool) list ->
+  string coq_object list
 
 (** {6 Generic search function} *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2e97b74d6..b1ed564d8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -517,7 +517,7 @@ let vernac_exact_proof c =
      called only at the begining of a proof. *)
   let status = by (Tactics.New.exact_proof c) in
   save_proof (Vernacexpr.Proved(true,None));
-  if not status then Pp.feedback Interface.AddedAxiom
+  if not status then Pp.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =
   let local = enforce_locality_exp locality local in
@@ -529,7 +529,7 @@ let vernac_assumption locality poly (local, kind) l nl =
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
   let status = do_assumptions kind nl l in
-  if not status then Pp.feedback Interface.AddedAxiom
+  if not status then Pp.feedback Feedback.AddedAxiom
 
 let vernac_record k poly finite infer struc binders sort nameopt cfs =
   let const = match nameopt with
@@ -795,7 +795,7 @@ let vernac_instance abst locality poly sup inst props pri =
   ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
 
 let vernac_context poly l =
-  if not (Classes.context poly l) then Pp.feedback Interface.AddedAxiom
+  if not (Classes.context poly l) then Pp.feedback Feedback.AddedAxiom
 
 let vernac_declare_instances locality ids pri =
   let glob = not (make_section_locality locality) in
@@ -825,7 +825,7 @@ let vernac_solve n tcom b =
     let p = Proof.maximal_unfocus command_focus p in
     p,status) in
     print_subgoals();
-    if not status then Pp.feedback Interface.AddedAxiom
+    if not status then Pp.feedback Feedback.AddedAxiom
  
 
   (* A command which should be a tactic. It has been