Merge PR#390: Updates to the Pretty Printing Infrastructure

90 files changed, 1346 insertions, 1855 deletions

diff --git a/Makefile.build b/Makefile.build
index 9d76638e1..01cc4d878 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -440,9 +440,9 @@ $(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkm
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \
+FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo	ide/document.cmo \
  ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \
- ide/xmlprotocol.cmo tools/fake_ide.cmo
+ ide/richpp.cmo ide/xmlprotocol.cmo tools/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ec16aa261..28c0126b4 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -176,9 +176,9 @@ let sort_cmp env univ pb s0 s1 =
         then begin
           if !Flags.debug then begin
             let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
-              (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
-               ++ Univ.pr_universes univ))
+            Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+               str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+               ++ Univ.pr_universes univ)
           end;
           raise NotConvertible
         end
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 12c3ec454..53e9a282f 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -70,6 +70,58 @@ work for EXTEND macros though.
 
 - The header parameter to `user_err` has been made optional.
 
+** Pretty printing **
+
+Some functions have been removed, see pretty printing below for more
+details.
+
+* Pretty Printing and XML protocol *
+
+The type std_cmdpps has been reworked and made the canonical "Coq rich
+document type". This allows for a more uniform handling of printing
+(specially in IDEs). The main consequences are:
+
+ - Richpp has been confined to IDE use. Most of previous uses of the
+   `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API
+   has been updated.
+
+ - The XML protocol will send a new message type of `pp`, which should
+   be rendered client-wise.
+
+ - `Set Printing Width` is deprecated, now width is controlled
+   client-side.
+
+ - `Pp_control` has removed. The new module `Topfmt` implements
+   console control for the toplevel.
+
+ - The impure tag system in Pp has been removed. This also does away
+   with the printer signatures and functors. Now printers tag
+   unconditionally.
+
+ - The following functions have been removed from `Pp`:
+
+   val stras : int * string -> std_ppcmds
+   val tbrk  : int * int -> std_ppcmds
+   val tab   : unit -> std_ppcmds
+   val pifb  : unit -> std_ppcmds
+   val comment  : int -> std_ppcmds
+   val comments : ((int * int) * string) list ref
+   val eval_ppcmds : std_ppcmds -> std_ppcmds
+   val is_empty : std_ppcmds -> bool
+   val t : std_ppcmds -> std_ppcmds
+   val hb : int -> std_ppcmds
+   val vb : int -> std_ppcmds
+   val hvb : int -> std_ppcmds
+   val hovb : int -> std_ppcmds
+   val tb : unit -> std_ppcmds
+   val close : unit -> std_ppcmds
+   val tclose : unit -> std_ppcmds
+   val open_tag : Tag.t -> std_ppcmds
+   val close_tag : unit -> std_ppcmds
+   val msg_with  : ...
+
+   module Tag
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index dc354b130..cd464801b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -29,7 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* std_ppcmds *)
-let pp   x = Pp.pp_with !Pp_control.std_ft x
+let pp   x = Pp.pp_with !Topfmt.std_ft x
 
 (** Future printer *)
 
diff --git a/engine/universes.ml b/engine/universes.ml
index 6720fcef8..30a9ef163 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -416,10 +416,9 @@ let constr_of_global gr =
 	(* Should be an error as we might forget constraints, allow for now
 	   to make firstorder work with "using" clauses *)
 	c
-      else raise (Invalid_argument 
-		    ("constr_of_global: globalization of polymorphic reference " ^ 
-			Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^
-			" would forget universes."))
+      else CErrors.user_err ~hdr:"constr_of_global"
+          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+	      str " would forget universes.")
     else c
 
 let constr_of_reference = constr_of_global
diff --git a/ide/coq.ml b/ide/coq.ml
index 6d44ca59e..3a1d87787 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -205,7 +205,7 @@ type handle = {
   proc : CoqTop.process;
   xml_oc : Xml_printer.t;
   mutable alive : bool;
-  mutable waiting_for : (ccb * logger) option; (* last call + callback + log *)
+  mutable waiting_for : ccb option; (* last call + callback *)
 }
 
 (** Coqtop process status :
@@ -290,18 +290,6 @@ let rec check_errors = function
 | `NVAL :: _ -> raise (TubeError "NVAL")
 | `OUT :: _ -> raise (TubeError "OUT")
 
-let handle_intermediate_message handle level content =
-  let logger  = match handle.waiting_for with
-    | Some (_, l) -> l
-    | None -> function
-        | Feedback.Error   -> fun s -> Minilib.log ~level:`ERROR   (xml_to_string s)
-        | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
-        | Feedback.Notice  -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
-        | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
-        | Feedback.Debug   -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
-  in
-  logger level content
-
 let handle_feedback feedback_processor xml =
   let feedback = Xmlprotocol.to_feedback xml in
   feedback_processor feedback
@@ -310,7 +298,7 @@ let handle_final_answer handle xml =
   let () = Minilib.log "Handling coqtop answer" in
   let ccb = match handle.waiting_for with
     | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml))
-    | Some (c, _) -> c in
+    | Some c -> c in
   let () = handle.waiting_for <- None in
   with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) }
 
@@ -332,18 +320,13 @@ 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;
-    match Xmlprotocol.is_message xml with
-    | Some (lvl, _loc, msg) ->
-      handle_intermediate_message handle lvl msg;
+    if Xmlprotocol.is_feedback xml then begin
+      handle_feedback feedback_processor xml;
       loop ()
-    | None ->
-      if Xmlprotocol.is_feedback xml then begin
-        handle_feedback feedback_processor xml;
-        loop ()
-      end else
-        begin
-          ignore (handle_final_answer handle xml)
-        end
+    end else
+      begin
+        ignore (handle_final_answer handle xml)
+      end
   in
   try loop ()
   with Xml_parser.Error _ as e ->
@@ -383,7 +366,7 @@ let bind_self_as f =
 (** This launches a fresh handle from its command line arguments. *)
 let spawn_handle args respawner feedback_processor =
   let prog = coqtop_path () in
-  let args = Array.of_list ("-async-proofs" :: "on" :: "-ideslave" :: args) in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
   let env =
     match !Flags.ideslave_coqtop_flags with
     | None -> None
@@ -493,20 +476,20 @@ let init_coqtop coqtop task =
 
 type 'a query = 'a Interface.value task
 
-let eval_call ?(logger=default_logger) call handle k =
+let eval_call call handle k =
   (** Send messages to coqtop and prepare the decoding of the answer *)
   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);
+  handle.waiting_for <- Some (mk_ccb (call,k));
   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 (Xmlprotocol.add x)
+let add x = eval_call (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 query x = eval_call (Xmlprotocol.query x)
 let mkcases s = eval_call (Xmlprotocol.mkcases s)
-let status ?logger force = eval_call ?logger (Xmlprotocol.status force)
+let status force = eval_call (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)
@@ -566,18 +549,11 @@ struct
 
   let _ = reset ()
 
-  (** Integer option *)
-
-  let width = ["Printing"; "Width"]
-  let width_state = ref None
-  let set_printing_width w = width_state := Some w
-
   (** Transmitting options to coqtop *)
 
   let enforce h k =
     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 (Xmlprotocol.set_options opts) h
       (function
 	| Interface.Good () -> k ()
@@ -585,8 +561,8 @@ struct
 
 end
 
-let goals ?logger x h k =
-  PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k)
+let goals x h k =
+  PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.goals x) h k)
 
 let 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 8a1fa3ed1..ab8c12a6f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -115,15 +115,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
 type 'a query = 'a Interface.value task
 (** A type abbreviation for coqtop specific answers *)
 
-val add        : ?logger:Ideutils.logger ->
-                 Interface.add_sty        -> Interface.add_rty query
+val add        : Interface.add_sty        -> Interface.add_rty query
 val edit_at    : Interface.edit_at_sty    -> Interface.edit_at_rty query
-val query      : ?logger:Ideutils.logger ->
-                 Interface.query_sty      -> Interface.query_rty query
-val status     : ?logger:Ideutils.logger ->
-                 Interface.status_sty     -> Interface.status_rty query
-val goals      : ?logger:Ideutils.logger ->
-                 Interface.goals_sty      -> Interface.goals_rty query
+val query      : Interface.query_sty      -> Interface.query_rty query
+val status     : Interface.status_sty     -> Interface.status_rty query
+val goals      : Interface.goals_sty      -> Interface.goals_rty query
 val evars      : Interface.evars_sty      -> Interface.evars_rty query
 val hints      : Interface.hints_sty      -> Interface.hints_rty query
 val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
@@ -143,7 +139,6 @@ sig
   val bool_items : bool_descr list
 
   val set : t -> bool -> unit
-  val set_printing_width : int -> unit
 
   (** [enforce] transmits to coq the current option values.
       It is also called by [goals] and [evars] above. *)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1563c7ffb..4a1d688f5 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -128,6 +128,9 @@ end = struct
 end
 open SentenceId
 
+let log_pp msg : unit task =
+  Coq.lift (fun () -> Minilib.log_pp msg)
+
 let log msg : unit task =
   Coq.lift (fun () -> Minilib.log msg)
 
@@ -162,13 +165,16 @@ let flags_to_color f =
   else if List.mem `INCOMPLETE f then `NAME "gray"
   else `NAME Preferences.processed_color#get
 
-let validate s =
-  let open Xml_datatype in
-  let rec validate = function
-  | PCData s -> Glib.Utf8.validate s
-  | Element (_, _, children) -> List.for_all validate children
-  in
-  validate (Richpp.repr s)
+(* Move to utils? *)
+let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with
+  | Pp.Ppcmd_empty
+  | Pp.Ppcmd_print_break _
+  | Pp.Ppcmd_force_newline  -> true
+  | Pp.Ppcmd_glue l    -> List.for_all validate l
+  | Pp.Ppcmd_string s  -> Glib.Utf8.validate s
+  | Pp.Ppcmd_box (_,s)
+  | Pp.Ppcmd_tag (_,s) -> validate s
+  | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s
 
 module Doc = Document
 
@@ -305,7 +311,7 @@ object(self)
 
   method private print_stack =
     Minilib.log "document:";
-    Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer)))
+    Minilib.log_pp (Doc.print document (dbg_to_string buffer))
 
   method private enter_focus start stop =
     let at id id' _ = Stateid.equal id' id in
@@ -337,7 +343,6 @@ object(self)
     buffer#get_iter_at_mark `INSERT
 
   method private show_goals_aux ?(move_insert=false) () =
-    Coq.PrintOpt.set_printing_width proof#width;
     if move_insert then begin
       let dest = self#get_start_of_input in
       if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin
@@ -345,7 +350,7 @@ object(self)
         script#recenter_insert
       end
     end;
-    Coq.bind (Coq.goals ~logger:messages#push ()) (function
+    Coq.bind (Coq.goals ()) (function
     | Fail x -> self#handle_failure_aux ~move_insert x
     | Good goals ->
       Coq.bind (Coq.evars ()) (function
@@ -368,7 +373,7 @@ object(self)
       else messages#add s;
     in
     let query =
-      Coq.query ~logger:messages#push (phrase,Stateid.dummy) in
+      Coq.query (phrase,Stateid.dummy) in
     let next = function
     | Fail (_, _, err) -> display_error err; Coq.return ()
     | Good msg ->
@@ -377,8 +382,7 @@ object(self)
     Coq.bind (Coq.seq action query) next
 
   method private mark_as_needed sentence =
-    Minilib.log("Marking " ^
-      Pp.string_of_ppcmds (dbg_to_string buffer false None sentence));
+    Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
     let to_process = Tags.Script.to_process in
@@ -418,9 +422,10 @@ object(self)
     | _ -> false
 
   method private enqueue_feedback msg =
+    (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
     let id = msg.id in
     if self#is_dummy_id id then () else Queue.add msg feedbacks
-    
+
   method private process_feedback () =
     let rec eat_feedback n =
       if n = 0 then true else
@@ -434,9 +439,11 @@ object(self)
           | _ -> None in
         try Some (Doc.find_map document finder)
         with Not_found -> None in
-      let log s state_id =
-        Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string
-          (Option.default Stateid.dummy state_id)) in
+      let log_pp s state_id =
+        Minilib.log_pp Pp.(seq
+                [str "Feedback "; s; str " on ";
+                 str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in
+      let log s state_id = log_pp (Pp.str s) state_id in
       begin match msg.contents, sentence with
       | AddedAxiom, Some (id,sentence) ->
           log "AddedAxiom" id;
@@ -466,22 +473,24 @@ object(self)
             (Printf.sprintf "%s %s %s" filepath ident ty)
       | Message(Error, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let msg = Richpp.raw_print msg         in
-          log "ErrorMsg" id;
+          log_pp Pp.(str "ErrorMsg" ++ msg) id;
           remove_flag sentence `PROCESSING;
-          add_flag sentence (`ERROR (loc, msg));
+          let rmsg = Pp.string_of_ppcmds msg     in
+          add_flag sentence (`ERROR (loc, rmsg));
           self#mark_as_needed sentence;
-          self#attach_tooltip sentence loc msg;
+          self#attach_tooltip sentence loc rmsg;
           if not (Loc.is_ghost loc) then
             self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
       | Message(Warning, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let msg = Richpp.raw_print msg         in
-          log "WarningMsg" id;
-          add_flag sentence (`WARNING (loc, msg));
-          self#attach_tooltip sentence loc msg;
-          self#position_warning_tag_at_sentence sentence loc
-      | Message((Info|Notice|Debug as lvl), _, msg), _ ->
+          log_pp Pp.(str "WarningMsg" ++ msg) id;
+          let rmsg = Pp.string_of_ppcmds msg     in
+          add_flag sentence (`WARNING (loc, rmsg));
+          self#attach_tooltip sentence loc rmsg;
+          self#position_warning_tag_at_sentence sentence loc;
+          messages#push Warning msg
+      | Message(lvl, loc, msg), Some (id,sentence) ->
+          log_pp Pp.(str "Msg" ++ msg) id;
           messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
@@ -628,10 +637,9 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-
-            logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
+            logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted");
             self#discard_command_queue queue;
-            conclude [] 
+            conclude []
         | `Skip(start,stop), (_,s) :: topstack ->
             assert(start#equal (buffer#get_iter_at_mark s.start));
             assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -641,11 +649,11 @@ object(self)
             add_flag sentence `PROCESSING;
             Doc.push document sentence;
             let _, _, phrase = self#get_sentence sentence in
-            let coq_query = Coq.add ~logger ((phrase,edit_id),(tip,verbose)) in
+            let coq_query = Coq.add ((phrase,edit_id),(tip,verbose)) in
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Feedback.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Pp.str msg);
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -653,7 +661,7 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Feedback.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Pp.str msg);
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
@@ -672,10 +680,10 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
+         messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
-   Coq.bind (Coq.status ~logger:messages#push true) next
+   Coq.bind (Coq.status true) next
 
   method stop_worker n =
     Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ())
@@ -859,7 +867,7 @@ object(self)
       let next = function
       | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
-        messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
+        messages#add (Pp.str ("Unsuccessfully tried: "^phrase));
         more
       | Good msg ->
         messages#add_string msg;
@@ -905,7 +913,7 @@ object(self)
     let get_initial_state =
       let next = function
       | Fail (_, _, message) ->
-        let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+        let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds message) in
         let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
         ignore (popup#run ()); exit 1
       | Good id -> initial_state <- id; Coq.return () in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index eec829f34..25858acce 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -318,7 +318,7 @@ let export kind sn =
         local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
         (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
       in
-      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+      sn.messages#set (Pp.str ("Running: "^cmd));
       let finally st = flash_info (cmd ^ pr_exit_status st)
       in
       run_command (fun msg -> sn.messages#add_string msg) finally cmd
@@ -431,7 +431,7 @@ let compile sn =
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+      sn.messages#set (Pp.str ("Running: "^cmd));
       let display s =
         sn.messages#add_string s;
         Buffer.add_string buf s
@@ -441,8 +441,8 @@ let compile sn =
           flash_info (f ^ " successfully compiled")
         else begin
           flash_info (f ^ " failed to compile");
-          sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
-          sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf));
+          sn.messages#set (Pp.str "Compilation output:\n");
+          sn.messages#add (Pp.str (Buffer.contents buf));
         end
       in
       run_command display finally cmd
@@ -464,7 +464,7 @@ let make sn =
     |Some f ->
       File.saveall ();
       let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
-      sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
+      sn.messages#set (Pp.str "Compilation output:\n");
       Buffer.reset last_make_buf;
       last_make := "";
       last_make_index := 0;
@@ -508,11 +508,11 @@ let next_error sn =
     let stopi = b#get_iter_at_byte ~line:(line-1) stop in
     b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
     b#place_cursor ~where:starti;
-    sn.messages#set (Richpp.richpp_of_string error_msg);
+    sn.messages#set (Pp.str error_msg);
     sn.script#misc#grab_focus ()
   with Not_found ->
     last_make_index := 0;
-    sn.messages#set (Richpp.richpp_of_string "No more errors.\n")
+    sn.messages#set (Pp.str "No more errors.\n")
 
 let next_error = cb_on_current_term next_error
 
@@ -536,7 +536,7 @@ let update_status sn =
     display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name);
     Coq.return ()
   in
-  Coq.bind (Coq.status ~logger:sn.messages#push false) next
+  Coq.bind (Coq.status false) next
 
 let find_next_occurrence ~backward sn =
   (** go to the next occurrence of the current word, forward or backward *)
@@ -789,7 +789,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 Feedback.Error (Richpp.richpp_of_string msg)
+        sn.messages#push Feedback.Error (Pp.str msg)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ok_cb in
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index ed1fa465d..043ad6008 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -2,7 +2,7 @@ Xml_lexer
 Xml_parser
 Xml_printer
 Serialize
-Richprinter
+Richpp
 Xmlprotocol
 Texmacspp
 Document
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 72a14134b..78b4c01e8 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,11 +9,12 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Serialize
-Richprinter
 Xml_lexer
 Xml_parser
 Xml_printer
+Serialize
+Richpp
+Topfmt
 Xmlprotocol
 Ideutils
 Coq
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ae3dcd94a..2ec79dc58 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -32,24 +32,6 @@ let init_signal_handler () =
   let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
   Sys.set_signal Sys.sigint (Sys.Signal_handle f)
 
-
-(** Redirection of standard output to a printable buffer *)
-
-let init_stdout, read_stdout =
-  let out_buff = Buffer.create 100 in
-  let out_ft = Format.formatter_of_buffer out_buff in
-  let deep_out_ft = Format.formatter_of_buffer out_buff in
-  let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
-  (fun () ->
-     flush_all ();
-     Pp_control.std_ft := out_ft;
-     Pp_control.err_ft := out_ft;
-     Pp_control.deep_ft := deep_out_ft;
-  ),
-  (fun () -> Format.pp_print_flush out_ft ();
-             let r = Buffer.contents out_buff in
-             Buffer.clear out_buff; r)
-
 let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let pr_error s = pr_with_pid s
@@ -115,24 +97,40 @@ let coqide_cmd_checks (loc,ast) =
 let add ((s,eid),(sid,verbose)) =
   let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
-  newid, (rc, read_stdout ())
+  (* TODO: the "" parameter is a leftover of the times the protocol
+   * used to include stderr/stdout output.
+   *
+   * Currently, we force all the output meant for the to go via the
+   * feedback mechanism, and we don't manipulate stderr/stdout, which
+   * are left to the client's discrection. The parameter is still there
+   * as not to break the core protocol for this minor change, but it should
+   * be removed in the next version of the protocol.
+   *)
+  newid, (rc, "")
 
 let edit_at id =
   match Stm.edit_at id with
   | `NewTip -> CSig.Inl ()
   | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))
 
-let query (s,id) = Stm.query ~at:id s; read_stdout ()
+(* TODO: the "" parameter is a leftover of the times the protocol
+ * used to include stderr/stdout output.
+ *
+ * Currently, we force all the output meant for the to go via the
+ * feedback mechanism, and we don't manipulate stderr/stdout, which
+ * are left to the client's discrection. The parameter is still there
+ * as not to break the core protocol for this minor change, but it should
+ * be removed in the next version of the protocol.
+ *)
+let query (s,id) = Stm.query ~at:id s; ""
 
 let annotate phrase =
   let (loc, ast) =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
     Vernac.parse_sentence (pa,None)
   in
-  let (_, xml) =
-    Richprinter.richpp_vernac ast
-  in
-  xml
+  (* XXX: Width should be a parameter of annotate... *)
+  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
 
 (** Goal display *)
 
@@ -192,13 +190,13 @@ let process_goal sigma g =
   let id = Goal.uid g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
+    pr_goal_concl_style_env env sigma norm_constr
   in
   let process_hyp d (env,l) =
     let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in
     let d' = CompactedDecl.to_named_context d in
       (List.fold_right Environ.push_named d' env,
-       (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in
+       (pr_compacted_decl env sigma d) :: l) in
   let (_env, hyps) =
     Context.Compacted.fold process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
@@ -214,8 +212,6 @@ let export_pre_goals pgs =
 
 let goals () =
   Stm.finish ();
-  let s = read_stdout () in
-  if not (String.is_empty s) then Feedback.msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
     Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
@@ -224,8 +220,6 @@ let goals () =
 let evars () =
   try
     Stm.finish ();
-    let s = read_stdout () in
-    if not (String.is_empty s) then Feedback.msg_info (str s);
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
     let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in
@@ -257,8 +251,6 @@ let status force =
       and display the other parts (opened sections and modules) *)
   Stm.finish ();
   if force then Stm.join ();
-  let s = read_stdout () in
-  if not (String.is_empty s) then Feedback.msg_info (str s);
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
@@ -281,7 +273,7 @@ let status force =
 let export_coq_object t = {
   Interface.coq_object_prefix = t.Search.coq_object_prefix;
   Interface.coq_object_qualid = t.Search.coq_object_qualid;
-  Interface.coq_object_object = t.Search.coq_object_object
+  Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
 }
 
 let pattern_of_string ?env s =
@@ -364,14 +356,10 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg () =
-    let msg = read_stdout () in
-    let msg = str msg ++ fnl () ++ CErrors.print ~info e in
-    Richpp.richpp_of_pp msg
-  in
+  let mk_msg () = CErrors.print ~info e in
   match e with
-  | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
-  | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
+  | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
+  | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
       | Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -409,7 +397,16 @@ let interp ((_raw, verbose), s) =
       | Some ast -> ast)
     () in
   Stm.interp verbose (vernac_parse s);
-  Stm.get_current_state (), CSig.Inl (read_stdout ())
+  (* TODO: the "" parameter is a leftover of the times the protocol
+   * used to include stderr/stdout output.
+   *
+   * Currently, we force all the output meant for the to go via the
+   * feedback mechanism, and we don't manipulate stderr/stdout, which
+   * are left to the client's discrection. The parameter is still there
+   * as not to break the core protocol for this minor change, but it should
+   * be removed in the next version of the protocol.
+   *)
+  Stm.get_current_state (), CSig.Inl ""
 
 (** When receiving the Quit call, we don't directly do an [exit 0],
     but rather set this reference, in order to send a final answer
@@ -428,14 +425,12 @@ let print_ast id =
 
 (** Grouping all call handlers together + error handling *)
 
-let eval_call xml_oc log c =
+let eval_call c =
   let interruptible f x =
     catch_break := true;
     Control.check_for_interrupt ();
     let r = f x in
     catch_break := false;
-    let out = read_stdout () in
-    if not (String.is_empty out) then log (str out);
     r
   in
   let handler = {
@@ -473,16 +468,8 @@ let print_xml =
     try Xml_printer.print oc xml; Mutex.unlock m
     with e -> let e = CErrors.push e in Mutex.unlock m; iraise e
 
-
-let slave_logger xml_oc ?loc level message =
-  (* convert the message into XML *)
-  let msg = hov 0 message in
-  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))         in
-  let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in
-  print_xml xml_oc xml
-
-let slave_feeder xml_oc msg =
-  let xml = Xmlprotocol.of_feedback msg in
+let slave_feeder fmt xml_oc msg =
+  let xml = Xmlprotocol.(of_feedback fmt msg) in
   print_xml xml_oc xml
 
 (** The main loop *)
@@ -491,17 +478,22 @@ let slave_feeder xml_oc msg =
     messages by [handle_exn] above. Otherwise, we die badly, without
     trying to answer malformed requests. *)
 
+let msg_format = ref (fun () ->
+    let margin = Option.default 72 (Topfmt.get_margin ()) in
+    Xmlprotocol.Richpp margin
+)
+
 let loop () =
   init_signal_handler ();
   catch_break := false;
-  let in_ch, out_ch = Spawned.get_channels () in
-  let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in
-  let in_lb = Lexing.from_function (fun s len ->
-    CThread.thread_friendly_read in_ch s ~off:0 ~len) in
-  let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
+  let in_ch, out_ch = Spawned.get_channels ()                        in
+  let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in
+  let in_lb         = Lexing.from_function (fun s len ->
+                      CThread.thread_friendly_read in_ch s ~off:0 ~len) in
+  (* SEXP parser make *)
+  let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
-  Feedback.set_logger (slave_logger xml_oc);
-  Feedback.add_feeder (slave_feeder xml_oc);
+  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -511,10 +503,10 @@ let loop () =
 (*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
       let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
-      let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) q in
+      let r  = eval_call q in
       let () = pr_debug_answer q r in
 (*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
-      print_xml xml_oc (Xmlprotocol.of_answer q r);
+      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);
       flush out_ch
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->
@@ -536,16 +528,19 @@ let loop () =
 let rec parse = function
   | "--help-XML-protocol" :: rest ->
         Xmlprotocol.document Xml_printer.to_string_fmt; exit 0
+  | "--xml_format=Ppcmds" :: rest ->
+        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest
   | x :: rest -> x :: parse rest
   | [] -> []
 
 let () = Coqtop.toploop_init := (fun args ->
         let args = parse args in
         Flags.make_silent true;
-        init_stdout ();
         CoqworkmgrApi.(init Flags.High);
         args)
 
 let () = Coqtop.toploop_run := loop
 
-let () = Usage.add_to_usage "coqidetop" "  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
+let () = Usage.add_to_usage "coqidetop"
+"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format
+  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c3a280796..da867e689 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -43,7 +43,7 @@ let xml_to_string xml =
   | Element (_, _, children) ->
     List.iter iter children
   in
-  let () = iter (Richpp.repr xml) in
+  let () = iter xml in
   Buffer.contents buf
 
 let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
@@ -75,7 +75,7 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
     let tags = try tag t :: tags with Not_found -> tags in
     List.iter (fun xml -> insert tags xml) children
   in
-  let () = try insert tags (Richpp.repr msg) with _ -> () in
+  let () = try insert tags msg with _ -> () in
   buf#delete_mark rmark
 
 let set_location = ref  (function s -> failwith "not ready")
@@ -327,7 +327,7 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Feedback.level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Pp.std_ppcmds -> unit
 
 let default_logger level message =
   let level = match level with
@@ -337,7 +337,7 @@ let default_logger level message =
   | Feedback.Warning -> `WARNING
   | Feedback.Error -> `ERROR
   in
-  Minilib.log ~level (xml_to_string message)
+  Minilib.log_pp ~level message
 
 
 (** {6 File operations} *)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index e32a4d9e3..4b4ba72b0 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,8 +52,6 @@ val pop_info : unit -> unit
 val clear_info : unit -> unit
 val flash_info : ?delay:int -> string -> unit
 
-val xml_to_string : Richpp.richpp -> string
-
 val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
@@ -69,7 +67,7 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Feedback.level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Pp.std_ppcmds -> unit
 
 val default_logger : logger
 (** Default logger. It logs messages that the casual user should not see. *)
diff --git a/ide/interface.mli b/ide/interface.mli
index 123cac6c2..9ed606258 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -12,15 +12,14 @@
 
 type raw = bool
 type verbose = bool
-type richpp = Richpp.richpp
 
 (** The type of coqtop goals *)
 type goal = {
   goal_id : string;
   (** Unique goal identifier *)
-  goal_hyp : richpp list;
+  goal_hyp : Pp.std_ppcmds list;
   (** List of hypotheses *)
-  goal_ccl : richpp;
+  goal_ccl : Pp.std_ppcmds;
   (** Goal conclusion *)
 }
 
@@ -119,7 +118,7 @@ type edit_id = Feedback.edit_id
    should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (state_id * location * richpp)
+  | Fail of (state_id * location * Pp.std_ppcmds)
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
@@ -128,9 +127,13 @@ type ('a, 'b) union = ('a, 'b) Util.union
 (**  [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid]
      on top of the current edit position (that is asserted to be [sid])
      verbosely if [v] is true.  The response [(id,(rc,s)] is the new state
-     [id] assigned to the phrase, some output [s].  [rc] is [Inl] if the new
+     [id] assigned to the phrase. [rc] is [Inl] if the new
      state id is the tip of the edit point, or [Inr tip] if the new phrase
-     closes a focus and [tip] is the new edit tip *)
+     closes a focus and [tip] is the new edit tip
+
+     [s] used to contain Coq's console output and has been deprecated
+     in favor of sending feedback, it will be removed in a future
+     version of the protocol.  *)
 type add_sty = (string * edit_id) * (state_id * verbose)
 type add_rty = state_id * ((unit, state_id) union * string)
 
@@ -143,8 +146,12 @@ type add_rty = state_id * ((unit, state_id) union * string)
 type edit_at_sty = state_id
 type edit_at_rty = (unit, state_id * (state_id * state_id)) union
 
-(** [query s id] executes [s] at state [id] and does not record any state
-    change but for the printings that are sent in response *)
+(** [query s id] executes [s] at state [id].
+
+    query used to reply with the contents of Coq's console output, and
+    has been deprecated in favor of sending the query answers as
+    feedback. It will be removed in a future version of the protocol.
+*)
 type query_sty = string * state_id
 type query_rty = string
 
@@ -203,7 +210,7 @@ type about_sty = unit
 type about_rty = coq_info
 
 type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * richpp
+type handle_exn_rty = state_id * location * Pp.std_ppcmds
 
 (* Retrocompatibility stuff *)
 type interp_sty = (raw * verbose) * string
diff --git a/ide/minilib.ml b/ide/minilib.ml
index d11e8c56b..2c24e46f8 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -30,7 +30,7 @@ let debug = ref false
    print in the response buffer.
 *)
 
-let log ?(level = `DEBUG) msg =
+let log_pp ?(level = `DEBUG) msg =
   let prefix = match level with
   | `DEBUG -> "DEBUG"
   | `INFO -> "INFO"
@@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg =
   | `FATAL -> "FATAL"
   in
   if !debug then begin
-    try Printf.eprintf "[%s] %s\n%!" prefix msg
+    try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg
     with _ -> ()
   end
 
+let log ?level str = log_pp ?level (Pp.str str)
+
 let coqify d = Filename.concat d "coq"
 
 let coqide_config_home () =
diff --git a/ide/minilib.mli b/ide/minilib.mli
index b7672c900..4517a2374 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -22,7 +22,8 @@ type level = [
 (** debug printing *)
 val debug : bool ref
 
-val log : ?level:level -> string -> unit
+val log_pp : ?level:level -> Pp.std_ppcmds -> unit
+val log    : ?level:level -> string        -> unit
 
 val coqide_config_home : unit -> string
 val coqide_config_dirs : unit -> string list
diff --git a/lib/richpp.ml b/ide/richpp.ml
index d1c6d158e..522a3e0b3 100644
--- a/lib/richpp.ml
+++ b/ide/richpp.ml
@@ -24,10 +24,6 @@ type 'a context = {
   (** Pending opened nodes *)
   mutable offset : int;
   (** Quantity of characters printed so far *)
-  mutable annotations : 'a option Int.Map.t;
-  (** Map associating annotations to indexes *)
-  mutable index : int;
-  (** Current index of annotations *)
 }
 
 (** We use Format to introduce tags inside the pretty-printed document.
@@ -38,23 +34,13 @@ type 'a context = {
     marking functions. As those functions are called when actually writing to
     the device, the resulting tree is correct.
 *)
-let rich_pp annotate ppcmds =
+let rich_pp width ppcmds =
 
   let context = {
     stack = Leaf;
     offset = 0;
-    annotations = Int.Map.empty;
-    index = (-1);
   } in
 
-  let pp_tag obj =
-    let index = context.index + 1 in
-    let () = context.index <- index in
-    let obj = annotate obj in
-    let () = context.annotations <- Int.Map.add index obj context.annotations in
-    string_of_int index
-  in
-
   let pp_buffer = Buffer.create 180 in
 
   let push_pcdata () =
@@ -81,12 +67,8 @@ let rich_pp annotate ppcmds =
     | Leaf -> assert false
     | Node (node, child, pos, ctx) ->
       let () = assert (String.equal tag node) in
-      let annotation =
-        try Int.Map.find (int_of_string node) context.annotations
-        with _ -> None
-      in
       let annotation = {
-        annotation = annotation;
+        annotation = Some tag;
         startpos = pos;
         endpos = context.offset;
       } in
@@ -113,18 +95,20 @@ let rich_pp annotate ppcmds =
   pp_set_formatter_tag_functions ft tag_functions;
   pp_set_mark_tags ft true;
 
-  (* Set formatter width. This is currently a hack and duplicate code
-     with Pp_control. Hopefully it will be fixed better in Coq 8.7 *)
-  let w = pp_get_margin str_formatter () in
-  let m = max (64 * w / 100) (w-30) in
-  pp_set_margin ft w;
+  (* Setting the formatter *)
+  pp_set_margin ft width;
+  let m = max (64 * width / 100) (width-30) in
   pp_set_max_indent ft m;
+  pp_set_max_boxes ft 50 ;
+  pp_set_ellipsis_text ft "...";
 
   (** The whole output must be a valid document. To that
       end, we nest the document inside <pp> tags. *)
+  pp_open_box ft 0;
   pp_open_tag ft "pp";
-  Pp.(pp_with ~pp_tag ft ppcmds);
+  Pp.(pp_with ft ppcmds);
   pp_close_tag ft ();
+  pp_close_box ft ();
 
   (** Get the resulting XML tree. *)
   let () = pp_print_flush ft () in
@@ -172,32 +156,14 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
 
 type richpp = xml
 
-let repr xml = xml
-let richpp_of_xml xml = xml
-let richpp_of_string s = PCData s
-
-let richpp_of_pp pp =
-  let annotate t = match Pp.Tag.prj t Ppstyle.tag with
-  | None -> None
-  | Some key -> Some (Ppstyle.repr key)
-  in
+let richpp_of_pp width pp =
   let rec drop = function
   | PCData s -> [PCData s]
   | Element (_, annotation, cs) ->
     let cs = List.concat (List.map drop cs) in
     match annotation.annotation with
     | None -> cs
-    | Some s -> [Element (String.concat "." s, [], cs)]
+    | Some s -> [Element (s, [], cs)]
   in
-  let xml = rich_pp annotate pp in
+  let xml = rich_pp width pp in
   Element ("_", [], drop xml)
-
-let raw_print xml =
-  let buf = Buffer.create 1024 in
-  let rec print = function
-  | PCData s -> Buffer.add_string buf s
-  | Element (_, _, cs) -> List.iter print cs
-  in
-  let () = print xml in
-  Buffer.contents buf
-
diff --git a/lib/richpp.mli b/ide/richpp.mli
index 287d265a8..ea4b189ba 100644
--- a/lib/richpp.mli
+++ b/ide/richpp.mli
@@ -16,14 +16,15 @@ type 'annotation located = {
   endpos     : int
 }
 
-(** [rich_pp get_annotations ppcmds] returns the interpretation
+(* XXX: The width parameter should be moved to a `formatter_property`
+   record shared with Topfmt *)
+
+(** [rich_pp width ppcmds] returns the interpretation
     of [ppcmds] as a semi-structured document
     that represents (located) annotations of this string.
     The [get_annotations] function is used to convert tags into the desired
-    annotation. *)
-val rich_pp :
-  (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds ->
-  'annotation located Xml_datatype.gxml
+    annotation. [width] sets the printing witdh of the formatter. *)
+val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml
 
 (** [annotations_positions ssdoc] returns a list associating each
     annotations with its position in the string from which [ssdoc] is
@@ -42,23 +43,9 @@ val xml_of_rich_pp :
 
 (** {5 Enriched text} *)
 
-type richpp
+type richpp = Xml_datatype.xml
+
 (** Type of text with style annotations *)
 
-val richpp_of_pp : Pp.std_ppcmds -> richpp
+val richpp_of_pp : int -> Pp.std_ppcmds -> richpp
 (** Extract style information from formatted text *)
-
-val richpp_of_xml : Xml_datatype.xml -> richpp
-(** Do not use outside of dedicated areas *)
-
-val richpp_of_string : string -> richpp
-(** Make a styled text out of a normal string *)
-
-val repr : richpp -> Xml_datatype.xml
-(** Observe the styled text as XML *)
-
-(** {5 Debug/Compat} *)
-
-(** Represent the semi-structured document as a string, dropping any additional
-    information. *)
-val raw_print : richpp -> string
diff --git a/ide/richprinter.ml b/ide/richprinter.ml
deleted file mode 100644
index 995cef1ac..000000000
--- a/ide/richprinter.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-open Richpp
-
-module RichppConstr = Ppconstr.Richpp
-module RichppVernac = Ppvernac.Richpp
-
-type rich_pp =
-    Ppannotation.t Richpp.located Xml_datatype.gxml
-    * Xml_datatype.xml
-
-let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
-
-let make_richpp pr ast =
-  let rich_pp =
-    rich_pp get_annotations (pr ast)
-  in
-  let xml = Ppannotation.(
-    xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
-  )
-  in
-  (rich_pp, xml)
-
-let richpp_vernac = make_richpp RichppVernac.pr_vernac
-let richpp_constr = make_richpp RichppConstr.pr_constr_expr
diff --git a/ide/richprinter.mli b/ide/richprinter.mli
deleted file mode 100644
index c9e84e3eb..000000000
--- a/ide/richprinter.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This module provides an entry point to "rich" pretty-printers that
-    produce pretty-printing as done by {!Printer} but with additional
-    annotations represented as a semi-structured document.
-
-    To understand what are these annotations and how they are represented
-    as standard XML attributes, please refer to {!Ppannotation}.
-
-    In addition to these annotations, each node of the semi-structured
-    document contains a [startpos] and an [endpos] attribute that
-    relate this node to the raw pretty-printing.
-    Please refer to {!Richpp} for more details. *)
-
-(** A rich pretty-print is composed of: *)
-type rich_pp =
-
-    (** - a generalized semi-structured document whose attributes are
-        annotations ; *)
-    Ppannotation.t Richpp.located Xml_datatype.gxml
-
-    (** - an XML document, representing annotations as usual textual
-        XML attributes. *)
-    * Xml_datatype.xml
-
-(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *)
-val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
-
-(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
-val richpp_constr : Constrexpr.constr_expr -> rich_pp
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 946aaf010..47dad8f19 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,18 +100,15 @@ object(self)
         if Str.string_match (Str.regexp "\\. *$") com 0 then com
         else com ^ " " ^ arg ^" . "
       in
-      let log level message =
-        Ideutils.insert_xml result#buffer message;
-        result#buffer#insert "\n";
-      in
       let process =
-	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
+	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
-            Ideutils.insert_xml result#buffer str;
+            let width = Ideutils.textview_width result in
+            Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str);
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
 	    Coq.return ()
           | Interface.Good res ->
-            result#buffer#insert res; 
+            result#buffer#insert res;
             notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
 	    Coq.return ())
       in
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 0330b8eff..3d0cd46cd 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -28,9 +28,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : Richpp.richpp -> unit
+    method add : Pp.std_ppcmds -> unit
     method add_string : string -> unit
-    method set : Richpp.richpp -> unit
+    method set : Pp.std_ppcmds -> unit
+    method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
@@ -57,46 +58,71 @@ let message_view () : message_view =
   let () = view#set_left_margin 2 in
   view#misc#show ();
   let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed cb in
-  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let _ = background_color#connect#changed ~callback:cb in
+  let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
-  object (self)
+
+  (* Inserts at point, advances the mark *)
+  let insert_msg (level, msg) =
+    let tags = match level with
+      | Feedback.Error   -> [Tags.Message.error]
+      | Feedback.Warning -> [Tags.Message.warning]
+      | _ -> []
+    in
+    let mark = `MARK mark in
+    let width = Ideutils.textview_width view in
+    Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp width msg);
+    buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"
+  in
+
+  let mv = object (self)
     inherit GObj.widget box#as_widget
 
+    (* List of displayed messages *)
+    val mutable last_width = -1
+    val mutable msgs = []
+
     val push = new GUtil.signal ()
 
     method connect =
       new message_view_signals_impl box#as_widget push
 
+    method refresh force =
+      (* We need to block updates here due to the following race:
+         insertion of messages may create a vertical scrollbar, this
+         will trigger a width change, calling refresh again and
+         going into an infinite loop. *)
+      let width = Ideutils.textview_width view  in
+      (* Could still this method race if the scrollbar changes the
+         textview_width ?? *)
+      let needed = force || last_width <> width in
+      if needed then begin
+        last_width <- width;
+        buffer#set_text "";
+        buffer#move_mark (`MARK mark) ~where:buffer#start_iter;
+        List.(iter insert_msg (rev msgs))
+      end
+
     method clear =
-      buffer#set_text "";
-      buffer#move_mark (`MARK mark) ~where:buffer#start_iter
+      msgs <- []; self#refresh true
 
     method push level msg =
-      let tags = match level with
-      | Feedback.Error -> [Tags.Message.error]
-      | Feedback.Warning -> [Tags.Message.warning]
-      | _ -> []
-      in
-      let rec non_empty = function
-      | Xml_datatype.PCData "" -> false
-      | Xml_datatype.PCData _ -> true
-      | Xml_datatype.Element (_, _, children) -> List.exists non_empty children
-      in
-      if non_empty (Richpp.repr msg) then begin
-        let mark = `MARK mark in
-        Ideutils.insert_xml ~mark buffer ~tags msg;
-        buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
-        push#call (level, msg)
-      end
+      msgs <- (level, msg) :: msgs;
+      insert_msg (level, msg);
+      push#call (level, msg)
 
     method add msg = self#push Feedback.Notice msg
 
-    method add_string s = self#add (Richpp.richpp_of_string s)
+    method add_string s = self#add (Pp.str s)
 
     method set msg = self#clear; self#add msg
 
     method buffer = text_buffer
 
   end
+  in
+  (* Is there a better way to connect the signal ? *)
+  let w_cb (_ : Gtk.rectangle) = mv#refresh false in
+  ignore (view#misc#connect#size_allocate ~callback:w_cb);
+  mv
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 2d34533de..d065fcbc8 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -18,9 +18,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : Richpp.richpp -> unit
+    method add : Pp.std_ppcmds -> unit
     method add_string : string -> unit
-    method set : Richpp.richpp -> unit
+    method set : Pp.std_ppcmds -> unit
+    method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 47c86045a..b5405570c 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -18,7 +18,6 @@ class type proof_view =
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
-    method width : int
   end
 
 (* tag is the tag to be hooked, item is the item covered by this tag, make_menu
@@ -74,6 +73,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
       | None -> [], []
       | Some (hl, h) -> (hl, h)
       in
+      let width = Ideutils.textview_width proof in
       let rec insert_hyp hints hs = match hs with
       | [] -> ()
       | hyp :: hs ->
@@ -84,7 +84,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           let () = hook_tag_cb tag hint sel_cb on_hover in
           [tag], hints
         in
-        let () = insert_xml ~tags proof#buffer hyp in
+        let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp width hyp) in
         proof#buffer#insert "\n";
         insert_hyp rem_hints hs
       in
@@ -98,13 +98,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        insert_xml proof#buffer cur_goal;
+        insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal);
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
         proof#buffer#insert (goal_str i goals_cnt);
-        insert_xml proof#buffer g;
+        insert_xml proof#buffer (Richpp.richpp_of_pp width g);
         proof#buffer#insert "\n"
       in
       let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
@@ -122,6 +122,7 @@ let rec flatten = function
 
 let display mode (view : #GText.view_skel) goals hints evars =
   let () = view#buffer#set_text "" in
+  let width = Ideutils.textview_width view in
   match goals with
   | None -> ()
     (* No proof in progress *)
@@ -144,7 +145,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* The proof is finished, with the exception of given up goals. *)
       view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
-        insert_xml view#buffer goal.Interface.goal_ccl;
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter given_up_goals;
@@ -153,7 +154,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
       let iter goal =
-        insert_xml view#buffer goal.Interface.goal_ccl;
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter shelved_goals
@@ -166,7 +167,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
         let () = view#buffer#insert (goal_str (succ i)) in
-        insert_xml view#buffer goal.Interface.goal_ccl;
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iteri iter bg
@@ -192,7 +193,7 @@ let proof_view () =
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
 
-  object
+  let pf = object
     inherit GObj.widget view#as_widget
     val mutable goals = None
     val mutable evars = None
@@ -207,9 +208,11 @@ let proof_view () =
 
     method refresh () =
       let dummy _ () = () in
-      display (mode_tactic dummy) (view :> GText.view_skel) goals None evars
-
-    method width = Ideutils.textview_width (view :> GText.view_skel)
+      display (mode_tactic dummy) view goals None evars
   end
-
-(*     ignore (proof_buffer#add_selection_clipboard cb); *)
+  in
+  (* Is there a better way to connect the signal ? *)
+  (* Can this be done in the object constructor? *)
+  let w_cb _ = pf#refresh () in
+  ignore (view#misc#connect#size_allocate w_cb);
+  pf
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index b6eae48b3..aa01d955d 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -14,7 +14,6 @@ class type proof_view =
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
-    method width : int
   end
 
 val proof_view : unit -> proof_view
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 5f82a8898..5f80d6897 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -12,6 +12,9 @@
 
 let protocol_version = "20150913"
 
+type msg_format = Richpp of int | Ppcmds
+let msg_format = ref (Richpp 72)
+
 (** * Interface of calls to Coq by CoqIde *)
 
 open Util
@@ -92,10 +95,57 @@ let to_stateid = function
 
 let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[])
 
-let of_richpp x = Element ("richpp", [], [Richpp.repr x])
-let to_richpp xml = match xml with
-  | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x
-  | x -> raise Serialize.(Marshal_error("richpp",x))
+let of_box (ppb : Pp.block_type) = let open Pp in match ppb with
+  | Pp_hbox   i -> constructor "ppbox" "hbox"   [of_int i]
+  | Pp_vbox   i -> constructor "ppbox" "vbox"   [of_int i]
+  | Pp_hvbox  i -> constructor "ppbox" "hvbox"  [of_int i]
+  | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i]
+
+let to_box = let open Pp in
+  do_match "ppbox" (fun s args -> match s with
+      | "hbox"   -> Pp_hbox   (to_int (singleton args))
+      | "vbox"   -> Pp_vbox   (to_int (singleton args))
+      | "hvbox"  -> Pp_hvbox  (to_int (singleton args))
+      | "hovbox" -> Pp_hovbox (to_int (singleton args))
+      | x        -> raise (Marshal_error("*ppbox",PCData x))
+    )
+
+let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with
+    | Ppcmd_empty         -> constructor "ppdoc" "emtpy"  []
+    | Ppcmd_string s      -> constructor "ppdoc" "string" [of_string s]
+    | Ppcmd_glue sl       -> constructor "ppdoc" "glue"   [of_list of_pp sl]
+    | Ppcmd_box (bt,s)    -> constructor "ppdoc" "box"    [of_pair of_box of_pp (bt,s)]
+    | Ppcmd_tag (t,s)     -> constructor "ppdoc" "tag"    [of_pair of_string of_pp (t,s)]
+    | Ppcmd_print_break (i,j)
+                          -> constructor "ppdoc" "break"     [of_pair of_int of_int (i,j)]
+    | Ppcmd_force_newline -> constructor "ppdoc" "newline"   []
+    | Ppcmd_comment cmd   -> constructor "ppdoc" "comment" [of_list of_string cmd]
+
+
+let rec to_pp xpp = let open Pp in
+  Pp.unrepr @@
+  do_match "ppdoc" (fun s args -> match s with
+    | "empty"     -> Ppcmd_empty
+    | "string"    -> Ppcmd_string (to_string (singleton args))
+    | "glue"      -> Ppcmd_glue (to_list to_pp (singleton args))
+    | "box"       -> let (bt,s) = to_pair to_box to_pp (singleton args) in
+                     Ppcmd_box(bt,s)
+    | "tag"       -> let (tg,s) = to_pair to_string to_pp (singleton args) in
+                     Ppcmd_tag(tg,s)
+    | "break"     -> let (i,j)   = to_pair to_int to_int (singleton args) in
+                     Ppcmd_print_break(i, j)
+    | "newline"   -> Ppcmd_force_newline
+    | "comment"   -> Ppcmd_comment (to_list to_string (singleton args))
+    | x           -> raise (Marshal_error("*ppdoc",PCData x))
+  ) xpp
+
+let of_richpp x = Element ("richpp", [], [x])
+
+(* Run-time Selectable *)
+let of_pp (pp : Pp.std_ppcmds) =
+  match !msg_format with
+  | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp)
+  | Ppcmds        -> of_pp pp
 
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
@@ -104,7 +154,7 @@ let of_value f = function
   | None -> []
   | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
   let id = of_stateid id in
-  Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg])
+  Element ("value", ["val", "fail"] @ loc, [id; of_pp msg])
 
 let to_value f = function
 | Element ("value", attrs, l) ->
@@ -120,7 +170,7 @@ let to_value f = function
     in
     let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in
     let id = to_stateid id in
-    let msg = to_richpp msg in
+    let msg = to_pp msg    in
     Fail (id, loc, msg)
   else raise (Marshal_error("good or fail",PCData ans))
 | x -> raise (Marshal_error("value",x))
@@ -147,15 +197,15 @@ let to_evar = function
   | x -> raise (Marshal_error("evar",x))
 
 let of_goal g =
-  let hyp = of_list of_richpp g.goal_hyp in
-  let ccl = of_richpp g.goal_ccl in
+  let hyp = of_list of_pp g.goal_hyp in
+  let ccl = of_pp 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_richpp hyp in
-    let ccl = to_richpp ccl in
-    let id = to_string id in
+    let hyp = to_list to_pp hyp in
+    let ccl = to_pp ccl         in
+    let id  = to_string id      in
     { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
   | x -> raise (Marshal_error("goal",x))
 
@@ -344,8 +394,8 @@ end = struct
         Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
     else
       let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-        "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^
-            Richpp.raw_print goal ^ "]" in
+        "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^
+            Pp.string_of_ppcmds goal ^ "]" in
       String.concat " " (List.map pr_goal g.fg_goals)
   let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
   let pr_status (s : status) =
@@ -631,6 +681,9 @@ let of_answer : type a. a call -> a value -> xml = function
   | PrintAst _   -> of_value (of_value_type print_ast_rty_t  )
   | Annotate _   -> of_value (of_value_type annotate_rty_t   )
 
+let of_answer msg_fmt =
+  msg_format := msg_fmt; of_answer
+
 let to_answer : type a. a call -> xml -> a value = function
   | Add _        -> to_value (to_value_type add_rty_t        )
   | Edit_at _    -> to_value (to_value_type edit_at_rty_t    )
@@ -701,10 +754,10 @@ let to_call : xml -> unknown_call =
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]"
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]"
   | Fail (id,Some(i,j),str) ->
       "FAIL "^Stateid.to_string id^
-        " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]"
+        " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with
   | Add _        -> pr_value_gen (print add_rty_t        ) value
@@ -760,7 +813,7 @@ let document to_string_fmt =
     (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),Richpp.richpp_of_string "error message"))));
+      (Fail (Stateid.initial,Some (15,34), Pp.str "error message"))));
   document_type_encoding to_string_fmt
 
 (* Moved from feedback.mli : This is IDE specific and we don't want to
@@ -787,20 +840,14 @@ let to_message_level =
 let of_message lvl loc msg =
   let lvl     = of_message_level lvl in
   let xloc    = of_option of_loc loc in
-  let content = of_richpp msg        in
+  let content = of_pp msg            in
   Xml_datatype.Element ("message", [], [lvl; xloc; content])
 
 let to_message xml = match xml with
   | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
-      Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
+      Message(to_message_level lvl, to_option to_loc xloc, to_pp content)
   | x -> raise (Marshal_error("message",x))
 
-let is_message xml =
-  try begin match to_message xml with
-    | Message(l,c,m) -> Some (l,c,m)
-    | _              -> None
-  end with | Marshal_error _ -> None
-
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "addedaxiom", _ -> AddedAxiom
   | "processed", _ -> Processed
@@ -870,6 +917,9 @@ let of_feedback msg =
   let route = string_of_int msg.route in
   Element ("feedback", obj @ ["route",route], [id;content])
 
+let of_feedback msg_fmt =
+  msg_format := msg_fmt; of_feedback
+
 let to_feedback xml = match xml with
   | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
       id = Edit(to_edit_id id);
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 1bb998970..9cefab517 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -40,12 +40,17 @@ val abstract_eval_call : handler -> 'a call -> 'a value
 
 val protocol_version : string
 
+(** By default, we still output messages in Richpp so we are
+    compatible with 8.6, however, 8.7 aware clients will want to
+    set this to Ppcmds *)
+type msg_format = Richpp of int | Ppcmds
+
 (** * XML data marshalling *)
 
 val of_call : 'a call -> xml
 val to_call : xml -> unknown_call
 
-val of_answer : 'a call -> 'a value -> xml
+val of_answer : msg_format -> 'a call -> 'a value -> xml
 val to_answer : 'a call -> xml -> 'a value
 
 (* Prints the documentation of this module *)
@@ -57,16 +62,8 @@ val pr_call : 'a call -> string
 val pr_value : 'a value -> string
 val pr_full_value : 'a call -> 'a value -> string
 
-(** * Serialization of rich documents *)
-val of_richpp : Richpp.richpp -> Xml_datatype.xml
-val to_richpp : Xml_datatype.xml -> Richpp.richpp
-
 (** * Serializaiton of feedback  *)
-val of_feedback : Feedback.feedback -> xml
+val of_feedback : msg_format -> Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback
-val is_feedback : xml -> bool
-
-val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option
-val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
-(* val to_message : xml -> Feedback.message *)
 
+val is_feedback : xml -> bool
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index dbebe6a48..99b763602 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -16,16 +16,6 @@ let push = Backtrace.add_backtrace
 
 exception Anomaly of string option * std_ppcmds (* System errors *)
 
-(* XXX: To move to common tagging functions in Pp, blocked on tag
- * system cleanup as we cannot define generic error tags now.
- *
- * Anyways, tagging should not happen here, but in the specific
- * listener to the msg_* stuff.
- *)
-let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
-let err_str       = tag_err_str "Error:"
-let ann_str       = tag_err_str "Anomaly:"
-
 let _ =
   let pr = function
   | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
@@ -102,7 +92,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (ann_str ++ raw_anomaly e ++ spc () ++
+    hov 0 (raw_anomaly e ++ spc () ++
            strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
            str ".")
   else
@@ -124,7 +114,7 @@ let iprint_no_report (e, info) =
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    hov 0 (err_str ++ where s ++ pps)
+    hov 0 (where s ++ pps)
   | _ -> raise Unhandled
 end
 
@@ -147,13 +137,3 @@ let handled e =
   let bottom _ = raise Bottom in
   try let _ = print_gen bottom !handle_stack e in true
   with Bottom -> false
-
-(** Prints info which is either an error or
-   an anomaly and then exits with the appropriate
-   error code *)
-
-let fatal_error info anomaly =
-  let msg = info ++ fnl () in
-  pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
-  Format.pp_print_flush !Pp_control.err_ft ();
-  exit (if anomaly then 129 else 1)
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 5cffc725d..0665a8ce7 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -98,8 +98,3 @@ val noncritical : exn -> bool
 (** Check whether an exception is handled by some toplevel printer. The
     [Anomaly] exception is never handled. *)
 val handled : exn -> bool
-
-(** Prints info which is either an error or
-   an anomaly and then exits with the appropriate
-   error code *)
-val fatal_error : Pp.std_ppcmds -> bool -> 'a
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 1e33173ee..c73ae9b90 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -15,7 +15,6 @@ Store
 Exninfo
 Backtrace
 IStream
-Pp_control
 Flags
 Control
 Loc
@@ -28,8 +27,6 @@ CStack
 Util
 Stateid
 Pp
-Ppstyle
-Richpp
 Feedback
 CUnix
 Envars
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 57c6f30a4..7d9d6bf7f 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -35,7 +35,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
   (* Generic messages *)
-  | Message of level * Loc.t option * Richpp.richpp
+  | Message of level * Loc.t option * Pp.std_ppcmds
 
 type feedback = {
   id : edit_or_state_id;
@@ -45,146 +45,16 @@ type feedback = {
 
 let default_route = 0
 
-(** Feedback and logging *)
-open Pp
-open Pp_control
-
-type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
-
-let msgnl_with ?pp_tag fmt strm = msg_with ?pp_tag fmt (strm ++ fnl ())
-
-(* XXX: This is really painful! *)
-module Emacs = struct
-
-  (* Special chars for emacs, to detect warnings inside goal output *)
-  let emacs_quote_start = String.make 1 (Char.chr 254)
-  let emacs_quote_end   = String.make 1 (Char.chr 255)
-
-  let emacs_quote_err g =
-    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
-
-  let emacs_quote_info_start = "<infomsg>"
-  let emacs_quote_info_end = "</infomsg>"
-
-  let emacs_quote_info g =
-    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
-
-end
-
-open Emacs
-
-let  dbg_str = tag Ppstyle.(Tag.inj debug_tag   tag) (str "Debug:")   ++ spc ()
-let info_str = mt ()
-let warn_str = tag Ppstyle.(Tag.inj warning_tag tag) (str "Warning:") ++ spc ()
-let  err_str = tag Ppstyle.(Tag.inj error_tag   tag) (str "Error:"  ) ++ spc ()
-
-let make_body quoter info ?loc s =
-  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
-  quoter (hov 0 (loc ++ info ++ s))
-
-(* Generic logger *)
-let gen_logger dbg err ?pp_tag ?loc level msg = match level with
-  | Debug   -> msgnl_with ?pp_tag !std_ft (make_body dbg  dbg_str ?loc msg)
-  | Info    -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg)
-  | Notice  -> msgnl_with ?pp_tag !std_ft msg
-  | Warning -> Flags.if_warn (fun () ->
-               msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) ()
-  | Error   -> msgnl_with ?pp_tag !err_ft (make_body err  err_str ?loc msg)
-
-(* We provide a generic clear_log_backend callback for backends
-   wanting to do clenaup after the print.
-*)
-let std_logger_tag     = ref None
-let std_logger_cleanup = ref (fun () -> ())
-
-let std_logger ?loc level msg =
-  gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg;
-  !std_logger_cleanup ()
-
-(* Rules for emacs:
-   - Debug/info: emacs_quote_info
-   - Warning/Error: emacs_quote_err
-   - Notice: unquoted
-
-  Note the inconsistency.
- *)
-let emacs_logger = gen_logger emacs_quote_info emacs_quote_err ?pp_tag:None
-
-(** Color logging. Moved from pp_style, it may need some more refactoring  *)
-
-(** Not thread-safe. We should put a lock somewhere if we print from
-    different threads. Do we? *)
-let make_style_stack () =
-  (** Default tag is to reset everything *)
-  let empty = Terminal.make () in
-  let default_tag = Terminal.({
-      fg_color = Some `DEFAULT;
-      bg_color = Some `DEFAULT;
-      bold = Some false;
-      italic = Some false;
-      underline = Some false;
-      negative = Some false;
-    })
-  in
-  let style_stack = ref [] in
-  let peek () = match !style_stack with
-  | []      -> default_tag  (** Anomalous case, but for robustness *)
-  | st :: _ -> st
-  in
-  let push tag =
-    let style = match Ppstyle.get_style tag with
-      | None    -> empty
-      | Some st -> st
-    in
-    (** Use the merging of the latest tag and the one being currently pushed.
-    This may be useful if for instance the latest tag changes the background and
-    the current one the foreground, so that the two effects are additioned. *)
-    let style = Terminal.merge (peek ()) style in
-    style_stack := style :: !style_stack;
-    Terminal.eval style
-  in
-  let pop _ = match !style_stack with
-  | []       -> (** Something went wrong, we fallback *)
-                Terminal.eval default_tag
-  | _ :: rem -> style_stack := rem;
-                Terminal.eval (peek ())
-  in
-  let clear () = style_stack := [] in
-  push, pop, clear
-
-let init_color_output () =
-  let open Pp_control in
-  let push_tag, pop_tag, clear_tag = make_style_stack () in
-  std_logger_cleanup := clear_tag;
-  std_logger_tag     := Some Ppstyle.pp_tag;
-  let tag_handler = {
-    Format.mark_open_tag   = push_tag;
-    Format.mark_close_tag  = pop_tag;
-    Format.print_open_tag  = ignore;
-    Format.print_close_tag = ignore;
-  } in
-  Format.pp_set_mark_tags !std_ft true;
-  Format.pp_set_mark_tags !err_ft true;
-  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
-  Format.pp_set_formatter_tag_functions !err_ft tag_handler
-
-let logger       = ref std_logger
-let set_logger l = logger := l
-
-let msg_info    ?loc x = !logger ?loc Info x
-let msg_notice  ?loc x = !logger ?loc Notice x
-let msg_warning ?loc x = !logger ?loc Warning x
-let msg_error   ?loc x = !logger ?loc Error x
-let msg_debug   ?loc x = !logger ?loc Debug x
-
 (** Feeders *)
-let feeders = ref []
-let add_feeder f = feeders := f :: !feeders
+let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7
 
-let debug_feeder = function
-  | { contents = Message (Debug, loc, pp) } ->
-       msg_debug ?loc (Pp.str (Richpp.raw_print pp))
-  | _ -> ()
+let add_feeder =
+  let f_id = ref 0 in fun f ->
+  incr f_id;
+  Hashtbl.add feeders !f_id f;
+  !f_id
+
+let del_feeder fid = Hashtbl.remove feeders fid
 
 let feedback_id    = ref (Edit 0)
 let feedback_route = ref default_route
@@ -198,34 +68,14 @@ let feedback ?id ?route what =
      route = Option.default !feedback_route route;
      id    = Option.default !feedback_id id;
   } in
-  List.iter (fun f -> f m) !feeders
+  Hashtbl.iter (fun _ f -> f m) feeders
 
+(* Logging messages *)
 let feedback_logger ?loc lvl msg =
-  feedback ~route:!feedback_route ~id:!feedback_id
-    (Message (lvl, loc, Richpp.richpp_of_pp msg))
-
-(* Output to file *)
-let ft_logger old_logger ft ?loc level mesg =
-  let id x = x in
-  match level with
-  | Debug   -> msgnl_with ft (make_body id  dbg_str mesg)
-  | Info    -> msgnl_with ft (make_body id info_str mesg)
-  | Notice  -> msgnl_with ft mesg
-  | Warning -> old_logger ?loc level mesg
-  | Error   -> old_logger ?loc level mesg
-
-let with_output_to_file fname func input =
-  let old_logger = !logger in
-  let channel = open_out (String.concat "." [fname; "out"]) in
-  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
-  try
-    let output = func input in
-    logger := old_logger;
-    close_out channel;
-    output
-  with reraise ->
-    let reraise = Backtrace.add_backtrace reraise in
-    logger := old_logger;
-    close_out channel;
-    Exninfo.iraise reraise
+  feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg))
 
+let msg_info    ?loc x = feedback_logger ?loc Info x
+let msg_notice  ?loc x = feedback_logger ?loc Notice x
+let msg_warning ?loc x = feedback_logger ?loc Warning x
+let msg_error   ?loc x = feedback_logger ?loc Error x
+let msg_debug   ?loc x = feedback_logger ?loc Debug x
diff --git a/lib/feedback.mli b/lib/feedback.mli
index b4bed8793..4bbdfcb5b 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -8,7 +8,7 @@
 
 open Xml_datatype
 
-(* Old plain messages (used to be in Pp) *)
+(* Legacy-style logging messages (used to be in Pp) *)
 type level =
   | Debug
   | Info
@@ -16,7 +16,6 @@ type level =
   | Warning
   | Error
 
-
 (** Coq "semantic" infos obtained during parsing/execution *)
 type edit_id = int
 type state_id = Stateid.t
@@ -44,7 +43,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
   (* Generic messages *)
-  | Message of level * Loc.t option * Richpp.richpp
+  | Message of level * Loc.t option * Pp.std_ppcmds
 
 type feedback = {
   id       : edit_or_state_id;  (* The document part concerned *)
@@ -53,37 +52,17 @@ type feedback = {
 }
 
 (** {6 Feedback sent, even asynchronously, to the user interface} *)
-
-(** Moved here from pp.ml *)
-
 (* Morally the parser gets a string and an edit_id, and gives back an AST.
  * Feedbacks during the parsing phase are attached to this edit_id.
  * The interpreter assignes an exec_id to the ast, and feedbacks happening
  * during interpretation are attached to the exec_id.
  * Only one among state_id and edit_id can be provided. *)
 
-(** A [logger] takes a level plus a pretty printing doc and logs it *)
-type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit
-
-(** [set_logger l] makes the [msg_*] to use [l] for logging *)
-val set_logger : logger -> unit
-
-(** [std_logger] standard logger to [stdout/stderr]  *)
-val std_logger : logger
-
-(** [init_color_output ()] Enable color in the std_logger *)
-val init_color_output : unit -> unit
-
-(** [feedback_logger] will produce feedback messages instead IO events *)
-val feedback_logger : logger
-val emacs_logger    : logger
+(** [add_feeder f] adds a feeder listiner [f], returning its id *)
+val add_feeder : (feedback -> unit) -> int
 
-
-(** [add_feeder] feeders observe the feedback *)
-val add_feeder : (feedback -> unit) -> unit
-
-(** Prints feedback messages of kind Message(Debug,_) using msg_debug *)
-val debug_feeder : feedback -> unit
+(** [del_feeder fid] removes the feeder with id [fid] *)
+val del_feeder : int -> unit
 
 (** [feedback ?id ?route fb] produces feedback fb, with [route] and
     [id] set appropiatedly, if absent, it will use the defaults set by
@@ -94,10 +73,6 @@ val feedback :
 (** [set_id_for_feedback route id] Set the defaults for feedback *)
 val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
 
-(** [with_output_to_file file f x] executes [f x] with logging
-    redirected to a file [file] *)
-val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-
 (** {6 output functions}
 
 [msg_notice] do not put any decoration on output by default. If
@@ -125,7 +100,3 @@ val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 
 val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit
 (** For debugging purposes *)
-
-
-
-
diff --git a/lib/pp.ml b/lib/pp.ml
index a51b4458f..9f33756df 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -6,64 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module Glue : sig
-
-  (** The [Glue] module implements a container data structure with
-      efficient concatenation. *)
-
-  type 'a t
-
-  val atom : 'a -> 'a t
-  val glue : 'a t -> 'a t -> 'a t
-  val empty : 'a t
-  val is_empty : 'a t -> bool
-  val iter : ('a -> unit) -> 'a t -> unit
-
-end = struct
-
-  type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t
-
-  let atom x = GLeaf x
-
-  let glue x y =
-    match x, y with
-    | GEmpty, _ -> y
-    | _, GEmpty -> x
-    | _, _ -> GNode (x,y)
-
-  let empty = GEmpty
-
-  let is_empty x = x = GEmpty
-
-  let rec iter f = function
-    | GEmpty -> ()
-    | GLeaf x -> f x
-    | GNode (x,y) -> iter f x; iter f y
-
-end
-
-module Tag :
-sig
-  type t 
-  type 'a key
-  val create : string -> 'a key
-  val inj : 'a -> 'a key -> t
-  val prj : t -> 'a key -> 'a option
-end =
-struct
-
-module Dyn = Dyn.Make(struct end)
-
-type t = Dyn.t
-type 'a key = 'a Dyn.tag
-let create = Dyn.create
-let inj = Dyn.Easy.inj
-let prj = Dyn.Easy.prj
-
-end
-
-open Pp_control
-
 (* The different kinds of blocks are:
    \begin{description}
    \item[hbox:] Horizontal block no line breaking;
@@ -75,45 +17,32 @@ open Pp_control
    \end{description}
  *)
 
+type pp_tag = string
+
 type block_type =
-  | Pp_hbox of int
-  | Pp_vbox of int
-  | Pp_hvbox of int
+  | Pp_hbox   of int
+  | Pp_vbox   of int
+  | Pp_hvbox  of int
   | Pp_hovbox of int
 
-type str_token =
-| Str_def of string
-| Str_len of string * int (** provided length *)
-
-type 'a ppcmd_token =
-  | Ppcmd_print of 'a
-  | Ppcmd_box of block_type * ('a ppcmd_token Glue.t)
+type doc_view =
+  | Ppcmd_empty
+  | Ppcmd_string of string
+  | Ppcmd_glue of doc_view list
+  | Ppcmd_box  of block_type * doc_view
+  | Ppcmd_tag of pp_tag * doc_view
+  (* Are those redundant? *)
   | Ppcmd_print_break of int * int
-  | Ppcmd_white_space of int
   | Ppcmd_force_newline
-  | Ppcmd_print_if_broken
-  | Ppcmd_open_box of block_type
-  | Ppcmd_close_box
   | Ppcmd_comment of string list
-  | Ppcmd_open_tag of Tag.t
-  | Ppcmd_close_tag
-
-type 'a ppdir_token =
-  | Ppdir_ppcmds of 'a ppcmd_token Glue.t
-  | Ppdir_print_newline
-  | Ppdir_print_flush
-
-type ppcmd = str_token ppcmd_token
 
-type std_ppcmds = ppcmd Glue.t
+(* Following discussion on #390, we play on the safe side and make the
+   internal representation opaque here. *)
+type t = doc_view
+type std_ppcmds = t
 
-type 'a ppdirs = 'a ppdir_token Glue.t
-
-let (++) = Glue.glue
-
-let app = Glue.glue
-
-let is_empty g = Glue.is_empty g
+let repr x = x
+let unrepr x = x
 
 (* Compute length of an UTF-8 encoded string
    Rem 1 : utf8_length <= String.length (equal if pure ascii)
@@ -151,23 +80,32 @@ let utf8_length s =
   done ;
   !cnt
 
+let app s1 s2 = match s1, s2 with
+  | Ppcmd_empty, s
+  | s, Ppcmd_empty -> s
+  | s1, s2         -> Ppcmd_glue [s1; s2]
+
+let seq s = Ppcmd_glue s
+
+let (++) = app
+
 (* formatting commands *)
-let str s = Glue.atom(Ppcmd_print (Str_def s))
-let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i)))
-let brk (a,b) = Glue.atom(Ppcmd_print_break (a,b))
-let fnl () = Glue.atom(Ppcmd_force_newline)
-let pifb () = Glue.atom(Ppcmd_print_if_broken)
-let ws n = Glue.atom(Ppcmd_white_space n)
-let comment l = Glue.atom(Ppcmd_comment l)
+let str s     = Ppcmd_string s
+let brk (a,b) = Ppcmd_print_break (a,b)
+let fnl  ()   = Ppcmd_force_newline
+let ws n      = Ppcmd_print_break (n,0)
+let comment l = Ppcmd_comment l
 
 (* derived commands *)
-let mt () = Glue.empty
-let spc () = Glue.atom(Ppcmd_print_break (1,0))
-let cut () = Glue.atom(Ppcmd_print_break (0,0))
-let align () = Glue.atom(Ppcmd_print_break (0,0))
-let int n = str (string_of_int n)
-let real r = str (string_of_float r)
-let bool b = str (string_of_bool b)
+let mt    () = Ppcmd_empty
+let spc   () = Ppcmd_print_break (1,0)
+let cut   () = Ppcmd_print_break (0,0)
+let align () = Ppcmd_print_break (0,0)
+let int   n  = str (string_of_int n)
+let real  r  = str (string_of_float r)
+let bool  b  = str (string_of_bool b)
+
+(* XXX: To Remove *)
 let strbrk s =
   let rec aux p n =
     if n < String.length s then
@@ -176,7 +114,7 @@ let strbrk s =
         else str (String.sub s p (n-p)) :: spc () :: aux (n+1) (n+1)
       else aux p (n + 1)
     else if p = n then [] else [str (String.sub s p (n-p))]
-  in List.fold_left (++) Glue.empty (aux 0 0)
+  in Ppcmd_glue (aux 0 0)
 
 let pr_loc_pos loc =
   if Loc.is_ghost loc then (str"<unknown>")
@@ -197,26 +135,16 @@ let pr_loc loc =
 	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
 	   str":" ++ fnl())
 
-let ismt = is_empty
+let ismt = function | Ppcmd_empty -> true | _ -> false
 
 (* boxing commands *)
-let h n s = Glue.atom(Ppcmd_box(Pp_hbox n,s))
-let v n s = Glue.atom(Ppcmd_box(Pp_vbox n,s))
-let hv n s = Glue.atom(Ppcmd_box(Pp_hvbox n,s))
-let hov n s = Glue.atom(Ppcmd_box(Pp_hovbox n,s))
-
-(* Opening and closing of boxes *)
-let hb n = Glue.atom(Ppcmd_open_box(Pp_hbox n))
-let vb n = Glue.atom(Ppcmd_open_box(Pp_vbox n))
-let hvb n = Glue.atom(Ppcmd_open_box(Pp_hvbox n))
-let hovb n = Glue.atom(Ppcmd_open_box(Pp_hovbox n))
-let close () = Glue.atom(Ppcmd_close_box)
+let h   n s = Ppcmd_box(Pp_hbox n,s)
+let v   n s = Ppcmd_box(Pp_vbox n,s)
+let hv  n s = Ppcmd_box(Pp_hvbox n,s)
+let hov n s = Ppcmd_box(Pp_hovbox n,s)
 
 (* Opening and closed of tags *)
-let open_tag t = Glue.atom(Ppcmd_open_tag t)
-let close_tag () = Glue.atom(Ppcmd_close_tag)
-let tag t s = open_tag t ++ s ++ close_tag ()
-let eval_ppcmds l = l
+let tag t s = Ppcmd_tag(t,s)
 
 (* In new syntax only double quote char is escaped by repeating it *)
 let escape_string s =
@@ -243,67 +171,34 @@ let rec pr_com ft s =
       Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
     | None -> ()
 
-type tag_handler = Tag.t -> Format.tag
-
 (* pretty printing functions *)
-let pp_dirs ?pp_tag ft =
-  let pp_open_box = function
+let pp_with ft =
+  let cpp_open_box = function
     | Pp_hbox n   -> Format.pp_open_hbox ft ()
     | Pp_vbox n   -> Format.pp_open_vbox ft n
     | Pp_hvbox n  -> Format.pp_open_hvbox ft n
     | Pp_hovbox n -> Format.pp_open_hovbox ft n
   in
-  let rec pp_cmd = function
-    | Ppcmd_print tok         ->
-        begin match tok with
-        | Str_def s ->
-          let n = utf8_length s in
-          Format.pp_print_as ft n s
-        | Str_len (s, n) ->
-          Format.pp_print_as ft n s
-        end
-    | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
-        pp_open_box bty ;
-        if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss;
-        Format.pp_close_box ft ()
-    | Ppcmd_open_box bty      -> pp_open_box bty
-    | Ppcmd_close_box         -> Format.pp_close_box ft ()
-    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
-    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
-    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
-    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft ()
+  let rec pp_cmd = let open Format in function
+    | Ppcmd_empty             -> ()
+    | Ppcmd_glue sl           -> List.iter pp_cmd sl
+    | Ppcmd_string str        -> let n = utf8_length str in
+                                 pp_print_as ft n str
+    | Ppcmd_box(bty,ss)       -> cpp_open_box bty ;
+                                 if not (over_max_boxes ()) then pp_cmd ss;
+                                 pp_close_box ft ()
+    | Ppcmd_print_break(m,n)  -> pp_print_break ft m n
+    | Ppcmd_force_newline     -> pp_force_newline ft ()
     | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
-    | Ppcmd_open_tag tag ->
-      begin match pp_tag with
-      | None -> ()
-      | Some f -> Format.pp_open_tag ft (f tag)
-      end
-    | Ppcmd_close_tag ->
-      begin match pp_tag with
-      | None -> ()
-      | Some _ -> Format.pp_close_tag ft ()
-      end
-  in
-  let pp_dir = function
-    | Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream
-    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
-    | Ppdir_print_flush      -> Format.pp_print_flush ft ()
+    | Ppcmd_tag(tag, s)       -> pp_open_tag  ft tag;
+                                 pp_cmd s;
+                                 pp_close_tag ft ()
   in
-  fun (dirstream : _ ppdirs) ->
-    try
-      Glue.iter pp_dir dirstream
-    with reraise ->
-      let reraise = Backtrace.add_backtrace reraise in
-      let () = Format.pp_print_flush ft () in
-      Exninfo.iraise reraise
-
-(* pretty printing functions WITHOUT FLUSH *)
-let pp_with ?pp_tag ft strm =
-  pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
-
-(* pretty printing functions WITH FLUSH *)
-let msg_with ?pp_tag ft strm =
-  pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
+  try pp_cmd
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    let () = Format.pp_print_flush ft () in
+    Exninfo.iraise reraise
 
 (* If mixing some output and a goal display, please use msg_warning,
    so that interfaces (proofgeneral for example) can easily dispatch
@@ -311,7 +206,7 @@ let msg_with ?pp_tag ft strm =
 
 (** Output to a string formatter *)
 let string_of_ppcmds c =
-  Format.fprintf Format.str_formatter "@[%a@]" (msg_with ?pp_tag:None) c;
+  Format.fprintf Format.str_formatter "@[%a@]" pp_with c;
   Format.flush_str_formatter ()
 
 (* Copy paste from Util *)
@@ -338,7 +233,7 @@ let pr_nth n =
 
 (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
 
-let prlist pr l = List.fold_left (fun x e -> x ++ pr e) Glue.empty l
+let prlist pr l = Ppcmd_glue (List.map pr l)
 
 (* unlike all other functions below, [prlist] works lazily.
    if a strict behavior is needed, use [prlist_strict] instead.
@@ -403,4 +298,3 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 let prvect elem v = prvect_with_sep mt elem v
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
-
diff --git a/lib/pp.mli b/lib/pp.mli
index f17908262..802ffe8e7 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,17 +6,65 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Pretty-printers. *)
+(** Coq document type. *)
+
+(** Pretty printing guidelines ******************************************)
+(*                                                                      *)
+(* `Pp.t` or `Pp.std_ppcmds` is the main pretty printing document type  *)
+(* in the Coq system. Documents are composed laying out boxes, and      *)
+(* users can add arbitrary tag metadata that backends are free          *)
+(*                                                                      *)
+(* The datatype has a public view to allow serialization or advanced    *)
+(* uses, however regular users are _strongly_ warned againt its use,    *)
+(* they should instead rely on the available functions below.           *)
+(*                                                                      *)
+(* Box order and number is indeed an important factor. Try to create    *)
+(* a proper amount of boxes. The `++` operator provides "efficient"     *)
+(* concatenation, but using the list constructors is usually preferred. *)
+(*                                                                      *)
+(* That is to say, this:                                                *)
+(*                                                                      *)
+(* `hov [str "Term"; hov (pr_term t); str "is defined"]`                *)
+(*                                                                      *)
+(* is preferred to:                                                     *)
+(*                                                                      *)
+(* `hov (str "Term" ++ hov (pr_term t) ++ str "is defined")`            *)
+(*                                                                      *)
+(************************************************************************)
 
-type std_ppcmds
+(* XXX: Improve and add attributes *)
+type pp_tag = string
+
+(* Following discussion on #390, we play on the safe side and make the
+   internal representation opaque here. *)
+type t
+type std_ppcmds = t
+
+type block_type =
+  | Pp_hbox   of int
+  | Pp_vbox   of int
+  | Pp_hvbox  of int
+  | Pp_hovbox of int
+
+type doc_view =
+  | Ppcmd_empty
+  | Ppcmd_string of string
+  | Ppcmd_glue of t list
+  | Ppcmd_box  of block_type * t
+  | Ppcmd_tag  of pp_tag * t
+  (* Are those redundant? *)
+  | Ppcmd_print_break of int * int
+  | Ppcmd_force_newline
+  | Ppcmd_comment of string list
+
+val repr   : std_ppcmds -> doc_view
+val unrepr : doc_view -> std_ppcmds
 
 (** {6 Formatting commands} *)
 
 val str   : string -> std_ppcmds
-val stras : int * string -> std_ppcmds
 val brk   : int * int -> std_ppcmds
 val fnl   : unit -> std_ppcmds
-val pifb  : unit -> std_ppcmds
 val ws    : int -> std_ppcmds
 val mt    : unit -> std_ppcmds
 val ismt  : std_ppcmds -> bool
@@ -28,15 +76,12 @@ val comment  : string list -> std_ppcmds
 val app : std_ppcmds -> std_ppcmds -> std_ppcmds
 (** Concatenation. *)
 
+val seq : std_ppcmds list -> std_ppcmds
+(** Multi-Concatenation. *)
+
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 (** Infix alias for [app]. *)
 
-val eval_ppcmds : std_ppcmds -> std_ppcmds
-(** Force computation. *)
-
-val is_empty : std_ppcmds -> bool
-(** Test emptyness. *)
-
 (** {6 Derived commands} *)
 
 val spc : unit -> std_ppcmds
@@ -57,42 +102,9 @@ val v : int -> std_ppcmds -> std_ppcmds
 val hv : int -> std_ppcmds -> std_ppcmds
 val hov : int -> std_ppcmds -> std_ppcmds
 
-(** {6 Opening and closing of boxes} *)
-
-val hb : int -> std_ppcmds
-val vb : int -> std_ppcmds
-val hvb : int -> std_ppcmds
-val hovb : int -> std_ppcmds
-val close : unit -> std_ppcmds
-
-(** {6 Opening and closing of tags} *)
-
-module Tag :
-sig
-  type t
-  (** Type of tags. Tags are dynamic types comparable to {Dyn.t}. *)
-
-  type 'a key
-  (** Keys used to inject tags *)
-
-  val create : string -> 'a key
-  (** Create a key with the given name. Two keys cannot share the same name, if
-      ever this is the case this function raises an assertion failure. *)
+(** {6 Tagging} *)
 
-  val inj : 'a -> 'a key -> t
-  (** Inject an object into a tag. *)
-
-  val prj : t -> 'a key -> 'a option
-  (** Project an object from a tag. *)
-end
-
-val tag : Tag.t -> std_ppcmds -> std_ppcmds
-val open_tag : Tag.t -> std_ppcmds
-val close_tag : unit -> std_ppcmds
-
-(** {6 Utilities} *)
-
-val string_of_ppcmds : std_ppcmds -> string
+val tag : pp_tag -> std_ppcmds -> std_ppcmds
 
 (** {6 Printing combinators} *)
 
@@ -159,16 +171,11 @@ val surround : std_ppcmds -> std_ppcmds
 (** Surround with parenthesis. *)
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-
 val pr_loc : Loc.t -> std_ppcmds
 
-(** {6 Low-level pretty-printing functions with and without flush} *)
+(** {6 Main renderers, to formatter and to string } *)
 
-(** FIXME: These ignore the logging settings and call [Format] directly *)
-type tag_handler = Tag.t -> Format.tag
+(** [pp_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
+val pp_with          : Format.formatter -> std_ppcmds -> unit
 
-(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt]  *)
-val msg_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
-
-(** [msg_with ?pp_tag fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
-val pp_with  : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
+val string_of_ppcmds : std_ppcmds -> string
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
deleted file mode 100644
index ab8dc0798..000000000
--- a/lib/pp_control.ml
+++ /dev/null
@@ -1,93 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Parameters of pretty-printing *)
-
-type pp_global_params = {
-  margin : int;
-  max_indent : int;
-  max_depth : int;
-  ellipsis : string }
-
-(* Default parameters of pretty-printing *)
-
-let dflt_gp = {
-  margin     = 78;
-  max_indent = 50;
-  max_depth  = 50;
-  ellipsis   = "..." }
-
-(* A deeper pretty-printer to print proof scripts *)
-
-let deep_gp = {
-  margin     = 78;
-  max_indent = 50;
-  max_depth  = 10000;
-  ellipsis   = "..." }
-
-(* set_gp : Format.formatter -> pp_global_params -> unit
- * set the parameters of a formatter *)
-
-let set_gp ft gp =
-  Format.pp_set_margin ft gp.margin ;
-  Format.pp_set_max_indent ft gp.max_indent ;
-  Format.pp_set_max_boxes ft gp.max_depth ;
-  Format.pp_set_ellipsis_text ft gp.ellipsis
-
-let set_dflt_gp ft = set_gp ft dflt_gp
-
-let get_gp ft =
-  { margin = Format.pp_get_margin ft ();
-    max_indent = Format.pp_get_max_indent ft ();
-    max_depth = Format.pp_get_max_boxes ft ();
-    ellipsis = Format.pp_get_ellipsis_text ft () }
-
-(* with_fp : 'a pp_formatter_params -> Format.formatter
- * returns of formatter for given formatter functions *)
-
-let with_fp chan out_function flush_function =
-  let ft = Format.make_formatter out_function flush_function in
-  Format.pp_set_formatter_out_channel ft chan;
-  ft
-
-(* Output on a channel ch *)
-
-let with_output_to ch =
-  let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in
-  set_gp ft deep_gp;
-  ft
-
-let std_ft = ref Format.std_formatter
-let _ = set_dflt_gp !std_ft
-
-let err_ft = ref Format.err_formatter
-let _ = set_gp !err_ft deep_gp
-
-let deep_ft = ref (with_output_to stdout)
-let _ = set_gp !deep_ft deep_gp
-
-(* For parametrization through vernacular *)
-let default = Format.pp_get_max_boxes !std_ft ()
-let default_margin = Format.pp_get_margin !std_ft ()
-
-let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ())
-let set_depth_boxes v =
-  Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v)
-
-let get_margin () = Some (Format.pp_get_margin !std_ft ())
-let set_margin v =
-  let v = match v with None -> default_margin | Some v -> v in
-  Format.pp_set_margin Format.str_formatter v;
-  Format.pp_set_margin !std_ft v;
-  Format.pp_set_margin !deep_ft v;
-  (* Heuristic, based on usage: the column on the right of max_indent
-     column is 20% of width, capped to 30 characters *)
-  let m = max (64 * v / 100) (v-30) in
-  Format.pp_set_max_indent Format.str_formatter m;
-  Format.pp_set_max_indent !std_ft m;
-  Format.pp_set_max_indent !deep_ft m
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
deleted file mode 100644
index aa47c5167..000000000
--- a/lib/ppstyle.ml
+++ /dev/null
@@ -1,73 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-module String = CString
-
-type t = string
-(** We use the concatenated string, with dots separating each string. We
-    forbid the use of dots in the strings. *)
-
-let tags : Terminal.style option String.Map.t ref = ref String.Map.empty
-
-let make ?style tag =
-  let check s = if String.contains s '.' then invalid_arg "Ppstyle.make" in
-  let () = List.iter check tag in
-  let name = String.concat "." tag in
-  let () = assert (not (String.Map.mem name !tags)) in
-  let () = tags := String.Map.add name style !tags in
-  name
-
-let repr t = String.split '.' t
-
-let get_style tag =
-  try String.Map.find tag !tags with Not_found -> assert false
-
-let set_style tag st =
-  try tags := String.Map.update tag st !tags with Not_found -> assert false
-
-let clear_styles () =
-  tags := String.Map.map (fun _ -> None) !tags
-
-let dump () = String.Map.bindings !tags
-
-let parse_config s =
-  let styles = Terminal.parse s in
-  let set accu (name, st) =
-    try String.Map.update name (Some st) accu with Not_found -> accu
-  in
-  tags := List.fold_left set !tags styles
-
-let tag = Pp.Tag.create "ppstyle"
-
-(** Default tag is to reset everything *)
-let default = Terminal.({
-  fg_color = Some `DEFAULT;
-  bg_color = Some `DEFAULT;
-  bold = Some false;
-  italic = Some false;
-  underline = Some false;
-  negative = Some false;
-})
-
-let empty = Terminal.make ()
-
-let error_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in
-  make ~style ["message"; "error"]
-
-let warning_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in
-  make ~style ["message"; "warning"]
-
-let debug_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in
-  make ~style ["message"; "debug"]
-
-let pp_tag t = match Pp.Tag.prj t tag with
-| None -> ""
-| Some key -> key
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
deleted file mode 100644
index d9fd75765..000000000
--- a/lib/ppstyle.mli
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Highlighting of printers. Used for pretty-printing terms that should be
-    displayed on a color-capable terminal. *)
-
-(** {5 Style tags} *)
-
-type t = string
-
-(** Style tags *)
-
-val make : ?style:Terminal.style -> string list -> t
-(** Create a new tag with the given name. Each name must be unique. The optional
-    style is taken as the default one. *)
-
-val repr : t -> string list
-(** Gives back the original name of the style tag where each string has been
-    concatenated and separated with a dot. *)
-
-val tag : t Pp.Tag.key
-(** An annotation for styles *)
-
-(** {5 Manipulating global styles} *)
-
-val get_style : t -> Terminal.style option
-(** Get the style associated to a tag. *)
-
-val set_style : t -> Terminal.style option -> unit
-(** Set a style associated to a tag. *)
-
-val clear_styles : unit -> unit
-(** Clear all styles. *)
-
-val parse_config : string -> unit
-(** Add all styles from the given string as parsed by {!Terminal.parse}.
-    Unregistered tags are ignored. *)
-
-val dump : unit -> (t * Terminal.style option) list
-(** Recover the list of known tags together with their current style. *)
-
-(** {5 Color output} *)
-
-val pp_tag : Pp.tag_handler
-(** Returns the name of a style tag that is understandable by the formatters
-    that have been inititialized through {!init_color_output}. To be used with
-    {!Pp.pp_with}. *)
-
-(** {5 Tags} *)
-
-val error_tag : t
-(** Tag used by the {!Pp.msg_error} function. *)
-
-val warning_tag : t
-(** Tag used by the {!Pp.msg_warning} function. *)
-
-val debug_tag : t
-(** Tag used by the {!Pp.msg_debug} function. *)
diff --git a/library/libobject.ml b/library/libobject.ml
index caa03c85b..8757ca08c 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -91,16 +91,8 @@ let declare_object_full odecl =
 			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
-(* The "try .. with .. " allows for correct printing when calling
-   declare_object a loading time.
-*)
-
-let declare_object odecl =
-  try fst (declare_object_full odecl)
-  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
-let declare_object_full odecl =
-  try declare_object_full odecl
-  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
+let declare_object odecl = fst (declare_object_full odecl)
+let declare_object_full odecl = declare_object_full odecl
 
 (* this function describes how the cache, load, open, and export functions
    are triggered. *)
diff --git a/library/summary.ml b/library/summary.ml
index 6efa07f38..2ec4760d6 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -107,8 +107,10 @@ let unfreeze_summaries fs =
     try fold id decl state
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
-      Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
-        (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
+      Feedback.msg_error
+        Pp.(seq [str "Error unfrezing summay %s\n%s\n%!";
+                 str (name_of_summary id);
+                 CErrors.iprint e]);
       iraise e
   in
   (** We rely on the order of the frozen list, and the order of folding *)
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 72bd11e03..3b84eaa81 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -105,7 +105,7 @@ module Error = struct
              Printf.sprintf "Unsupported Unicode character (0x%x)" x)
 
   (* Require to fix the Camlp4 signature *)
-  let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x))
+  let print ppf x = Pp.pp_with ppf (Pp.str (to_string x))
 
 end
 open Error
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0a591e786..fc8d5356c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -67,7 +67,9 @@ let pp_boxed_tuple f = function
     blocks is less that a line length. To avoid this awkward situation,
     we attach a big virtual size to [fnl] newlines. *)
 
-let fnl () = stras (1000000,"") ++ fnl ()
+(* EG: This looks quite suspicious... but beware of bugs *)
+(* let fnl () = stras (1000000,"") ++ fnl () *)
+let fnl () = fnl ()
 
 let fnl2 () = fnl () ++ fnl ()
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index e019bb3c2..2b12462ad 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -472,13 +472,14 @@ let formatter dry file =
     if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
     else
       match file with
-	| Some f -> Pp_control.with_output_to f
+	| Some f -> Topfmt.with_output_to f
 	| None -> Format.formatter_of_buffer buf
   in
+  (* XXX: Fixme, this shouldn't depend on Topfmt *)
   (* We never want to see ellipsis ... in extracted code *)
   Format.pp_set_max_boxes ft max_int;
   (* We reuse the width information given via "Set Printing Width" *)
-  (match Pp_control.get_margin () with
+  (match Topfmt.get_margin () with
     | None -> ()
     | Some i ->
       Format.pp_set_margin ft i;
@@ -518,8 +519,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
     set_phase Impl;
     pp_with ft (d.preamble mo comment opened unsafe_needs);
     pp_with ft (d.pp_struct struc);
+    Format.pp_print_flush ft ();
     Option.iter close_out cout;
   with reraise ->
+    Format.pp_print_flush ft ();
     Option.iter close_out cout; raise reraise
   end;
   if not dry then Option.iter info_file fn;
@@ -532,8 +535,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 set_phase Intf;
 	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
 	 pp_with ft (d.pp_sig (signature_of_structure struc));
+         Format.pp_print_flush ft ();
 	 close_out cout;
        with reraise ->
+         Format.pp_print_flush ft ();
 	 close_out cout; raise reraise
        end;
        info_file si)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d89bf95ee..d8e382155 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -66,7 +66,7 @@ let pp_header_comment = function
   | None -> mt ()
   | Some com -> pp_comment com ++ fnl2 ()
 
-let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl ()
+let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl ()
 
 let pp_tdummy usf =
   if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
@@ -618,7 +618,7 @@ and pp_module_type params = function
       push_visible mp params;
       let try_pp_specif l x =
         let px = pp_specif x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_specif *)
       let l = List.fold_left try_pp_specif [] sign in
@@ -696,7 +696,7 @@ and pp_module_expr params = function
       push_visible mp params;
       let try_pp_structure_elem l x =
         let px = pp_structure_elem x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_structure_elem *)
       let l = List.fold_left try_pp_structure_elem [] sel in
@@ -714,7 +714,7 @@ let rec prlist_sep_nonempty sep f = function
   | h::t ->
      let e = f h in
      let r = prlist_sep_nonempty sep f t in
-     if Pp.is_empty e then r
+     if Pp.ismt e then r
      else e ++ sep () ++ r
 
 let do_struct f s =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6f4ef37b4..dc418d530 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -27,6 +27,26 @@ open Pputils
 open Ppconstr
 open Printer
 
+module Tag =
+struct
+
+  let keyword   = "tactic.keyword"
+  let primitive = "tactic.primitive"
+  let string    = "tactic.string"
+
+end
+
+let tag t s = Pp.tag t s
+let do_not_tag _ x = x
+let tag_keyword                 = tag Tag.keyword
+let tag_primitive               = tag Tag.primitive
+let tag_string                  = tag Tag.string
+let tag_glob_tactic_expr        = do_not_tag
+let tag_glob_atomic_tactic_expr = do_not_tag
+let tag_raw_tactic_expr         = do_not_tag
+let tag_raw_atomic_tactic_expr  = do_not_tag
+let tag_atomic_tactic_expr      = do_not_tag
+
 let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type 'a grammar_tactic_prod_item_expr =
@@ -64,30 +84,6 @@ type 'a extra_genarg_printer =
     (tolerability -> Val.t -> std_ppcmds) ->
     'a -> std_ppcmds
 
-module Make
-  (Ppconstr : Ppconstrsig.Pp)
-  (Taggers : sig
-      val tag_keyword
-        : std_ppcmds -> std_ppcmds
-      val tag_primitive
-        : std_ppcmds -> std_ppcmds
-      val tag_string
-        : std_ppcmds -> std_ppcmds
-      val tag_glob_tactic_expr
-        : glob_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_glob_atomic_tactic_expr
-        : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_raw_tactic_expr
-        : raw_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_raw_atomic_tactic_expr
-        : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_atomic_tactic_expr
-        : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-  end)
-= struct
-
-  open Taggers
-
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
@@ -1206,37 +1202,6 @@ module Make
 
   let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
 
-end
-
-module Tag =
-struct
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["tactic"; "keyword"]
-
-  let primitive =
-    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
-    Ppstyle.make ~style ["tactic"; "primitive"]
-
-  let string =
-    let style = Terminal.make ~fg_color:`LIGHT_RED () in
-    Ppstyle.make ~style ["tactic"; "string"]
-
-end
-
-include Make (Ppconstr) (struct
-    let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
-    let do_not_tag _ x = x
-    let tag_keyword                 = tag Tag.keyword
-    let tag_primitive               = tag Tag.primitive
-    let tag_string                  = tag Tag.string
-    let tag_glob_tactic_expr        = do_not_tag
-    let tag_glob_atomic_tactic_expr = do_not_tag
-    let tag_raw_tactic_expr         = do_not_tag
-    let tag_raw_atomic_tactic_expr  = do_not_tag
-    let tag_atomic_tactic_expr      = do_not_tag
-end)
-
 let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
   (g : 'b glob_extra_genarg_printer)
@@ -1338,22 +1303,3 @@ let () =
   let pr_unit _ _ _ () = str "()" in
   let printer _ _ prtac = prtac (0, E) in
   declare_extra_genarg_pprule wit_ltac printer printer pr_unit
-
-module Richpp = struct
-
-  include Make (Ppconstr.Richpp) (struct
-    open Ppannotation
-    open Genarg
-    let do_not_tag _ x = x
-    let tag e s = Pp.tag (Pp.Tag.inj e tag) s
-    let tag_keyword                   = tag AKeyword
-    let tag_primitive                 = tag AKeyword
-    let tag_string                    = do_not_tag ()
-    let tag_glob_tactic_expr        e = tag (AGlbGenArg (in_gen (glbwit wit_ltac) e))
-    let tag_glob_atomic_tactic_expr   = do_not_tag
-    let tag_raw_tactic_expr         e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e))
-    let tag_raw_atomic_tactic_expr    = do_not_tag
-    let tag_atomic_tactic_expr        = do_not_tag
-  end)
-
-end
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 86e3ea548..43e22dba3 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -13,6 +13,8 @@ open Pp
 open Genarg
 open Geninterp
 open Names
+open Misctypes
+open Environ
 open Constrexpr
 open Tacexpr
 open Ppextend
@@ -54,14 +56,66 @@ type pp_tactic = {
 
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as raw strings. *)
-include Pptacticsig.Pp
+val pr_with_occurrences :
+  ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+val pr_red_expr :
+  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+  ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+val pr_may_eval :
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+
+val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+
+val pr_in_clause :
+  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_clauses :  bool option ->
+  ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+val pr_raw_extend: env -> int ->
+  ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+val pr_glob_extend: env -> int ->
+  ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
+
+val pr_extend :
+  (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+val pr_alias_key : Names.KerName.t -> std_ppcmds
+
+val pr_alias : (Val.t -> std_ppcmds) ->
+  int -> Names.KerName.t -> Val.t list -> std_ppcmds
+
+val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
+val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+
+val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
+
+val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+
+val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
+
+val pr_hintbases : string list option -> std_ppcmds
+
+val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+
+val pr_bindings :
+  ('constr -> std_ppcmds) ->
+  ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
+
+val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('b, 'a) match_rule -> std_ppcmds
+
+val pr_value : tolerability -> Val.t -> std_ppcmds
 
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as annotated strings. The annotations can be
-    retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}. *)
-module Richpp : Pptacticsig.Pp
 
 val ltop : tolerability
diff --git a/plugins/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli
deleted file mode 100644
index 74ddd377a..000000000
--- a/plugins/ltac/pptacticsig.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Genarg
-open Geninterp
-open Tacexpr
-open Ppextend
-open Environ
-open Misctypes
-
-module type Pp = sig
-
-  val pr_with_occurrences :
-    ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
-  val pr_red_expr :
-    ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
-    ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
-  val pr_may_eval :
-    ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-    ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
-
-  val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-
-  val pr_in_clause :
-    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
-  val pr_clauses :  bool option ->
-    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
-  val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
-
-  val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
-
-  val pr_raw_extend: env -> int ->
-    ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
-
-  val pr_glob_extend: env -> int ->
-    ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
-
-  val pr_extend :
-    (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
-
-  val pr_alias_key : Names.KerName.t -> std_ppcmds
-
-  val pr_alias : (Val.t -> std_ppcmds) ->
-    int -> Names.KerName.t -> Val.t list -> std_ppcmds
-
-  val pr_alias_key : Names.KerName.t -> std_ppcmds
-
-  val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
-
-  val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
-
-  val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
-
-  val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
-
-  val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
-
-  val pr_hintbases : string list option -> std_ppcmds
-
-  val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
-
-  val pr_bindings :
-    ('constr -> std_ppcmds) ->
-    ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
-
-  val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
-
-  val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-    ('b, 'a) match_rule -> std_ppcmds
-
-  val pr_value : tolerability -> Val.t -> std_ppcmds
-
-end
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 8b9261113..1ad4d622b 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -505,12 +505,12 @@ let pp_mapint map =
 		pp_form obj ++ str " => " ++
 				 pp_list (fun (i,f) -> pp_form f) l ++
 				 cut ()) ) map;
-    str "{ " ++ vb 0 ++  (!pp) ++ str " }" ++ close ()
+    str "{ " ++ hv 0 (!pp ++ str " }")
 
 let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
 
 let pp_gl gl= cut () ++
-  str "{ " ++ vb 0 ++
+  str "{ " ++ hv 0 (
 	      begin
 		match gl.abs with
 		    None -> str ""
@@ -520,7 +520,7 @@ let pp_gl gl= cut () ++
   str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
   str "arrows=" ++ pp_mapint gl.right ++ cut () ++
   str "cnx   =" ++ pp_list pp_connect gl.cnx ++ cut () ++
-  str "goal  =" ++ pp_form gl.gl ++ str " }" ++ close ()
+  str "goal  =" ++ pp_form gl.gl ++ str " }")
 
 let pp =
   function
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
deleted file mode 100644
index 726c0ffcf..000000000
--- a/printing/ppannotation.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Ppextend
-open Constrexpr
-open Vernacexpr
-open Genarg
-
-type t =
-  | AKeyword
-  | AUnparsing            of unparsing
-  | AConstrExpr           of constr_expr
-  | AVernac               of vernac_expr
-  | AGlbGenArg            of glob_generic_argument
-  | ARawGenArg            of raw_generic_argument
-
-let tag_of_annotation = function
-  | AKeyword                -> "keyword"
-  | AUnparsing _            -> "unparsing"
-  | AConstrExpr _           -> "constr_expr"
-  | AVernac _               -> "vernac_expr"
-  | AGlbGenArg _            -> "glob_generic_argument"
-  | ARawGenArg _            -> "raw_generic_argument"
-
-let attributes_of_annotation a =
-  []
-
-let tag = Pp.Tag.create "ppannotation"
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
deleted file mode 100644
index b0e0facef..000000000
--- a/printing/ppannotation.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This module defines the annotations that are attached to
-    semi-structured pretty-printing of Coq syntactic objects. *)
-
-open Ppextend
-open Constrexpr
-open Vernacexpr
-open Genarg
-
-type t =
-  | AKeyword
-  | AUnparsing            of unparsing
-  | AConstrExpr           of constr_expr
-  | AVernac               of vernac_expr
-  | AGlbGenArg            of glob_generic_argument
-  | ARawGenArg            of raw_generic_argument
-
-val tag_of_annotation : t -> string
-
-val attributes_of_annotation : t -> (string * string) list
-
-val tag : t Pp.Tag.key
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 80ddd669f..d92d83275 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -21,18 +21,31 @@ open Decl_kinds
 open Misctypes
 (*i*)
 
-module Make (Taggers : sig
-  val tag_keyword     : std_ppcmds -> std_ppcmds
-  val tag_evar     : std_ppcmds -> std_ppcmds
-  val tag_type     : std_ppcmds -> std_ppcmds
-  val tag_path     : std_ppcmds -> std_ppcmds
-  val tag_ref     : std_ppcmds -> std_ppcmds
-  val tag_var     : std_ppcmds -> std_ppcmds
-  val tag_constr_expr : constr_expr -> std_ppcmds -> std_ppcmds
-  val tag_unparsing   : unparsing -> std_ppcmds -> std_ppcmds
-end) = struct
-
-  open Taggers
+module Tag =
+struct
+  let keyword   = "constr.keyword"
+  let evar      = "constr.evar"
+  let univ      = "constr.type"
+  let notation  = "constr.notation"
+  let variable  = "constr.variable"
+  let reference = "constr.reference"
+  let path      = "constr.path"
+
+end
+
+let do_not_tag _ x = x
+let tag t s = Pp.tag t s
+let tag_keyword     = tag Tag.keyword
+let tag_evar        = tag Tag.evar
+let tag_type        = tag Tag.univ
+let tag_unparsing   = function
+| UnpTerminal s -> tag Tag.notation
+| _ -> do_not_tag ()
+let tag_constr_expr = do_not_tag
+let tag_path = tag Tag.path
+let tag_ref = tag Tag.reference
+let tag_var = tag Tag.variable
+
 
   let keyword s = tag_keyword (str s)
   let sep_v = fun _ -> str"," ++ spc()
@@ -764,86 +777,3 @@ end) = struct
 
   let pr_binders = pr_undelimited_binders spc (pr ltop)
 
-end
-
-module Tag =
-struct
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["constr"; "keyword"]
-
-  let evar =
-    let style = Terminal.make ~fg_color:`LIGHT_BLUE () in
-    Ppstyle.make ~style ["constr"; "evar"]
-
-  let univ =
-    let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in
-    Ppstyle.make ~style ["constr"; "type"]
-
-  let notation =
-    let style = Terminal.make ~fg_color:`WHITE () in
-    Ppstyle.make ~style ["constr"; "notation"]
-
-  let variable =
-    Ppstyle.make ["constr"; "variable"]
-
-  let reference =
-    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
-    Ppstyle.make ~style ["constr"; "reference"]
-
-  let path =
-    let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in
-    Ppstyle.make ~style ["constr"; "path"]
-
-end
-
-let do_not_tag _ x = x
-
-let split_token tag s =
-  let len = String.length s in
-  let rec parse_string off i =
-    if Int.equal i len then
-      if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
-    else if s.[i] == ' ' then
-      if Int.equal off i then parse_space 1 (succ i)
-      else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
-    else parse_string off (succ i)
-  and parse_space spc i =
-    if Int.equal i len then str (String.make spc ' ')
-    else if s.[i] == ' ' then parse_space (succ spc) (succ i)
-    else str (String.make spc ' ') ++ parse_string i (succ i)
-  in
-  parse_string 0 0
-
-(** Instantiating Make with tagging functions that only add style
-    information. *)
-include Make (struct
-    let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
-    let tag_keyword     = tag Tag.keyword
-    let tag_evar        = tag Tag.evar
-    let tag_type        = tag Tag.univ
-    let tag_unparsing   = function
-    | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
-    | _ -> do_not_tag ()
-    let tag_constr_expr = do_not_tag
-    let tag_path = tag Tag.path
-    let tag_ref = tag Tag.reference
-    let tag_var = tag Tag.variable
-end)
-
-module Richpp = struct
-
-  include Make (struct
-    open Ppannotation
-    let tag_keyword       = Pp.tag (Pp.Tag.inj AKeyword tag)
-    let tag_type          = Pp.tag (Pp.Tag.inj AKeyword tag)
-    let tag_evar          = do_not_tag ()
-    let tag_unparsing unp = Pp.tag (Pp.Tag.inj (AUnparsing unp) tag)
-    let tag_constr_expr e = Pp.tag (Pp.Tag.inj (AConstrExpr e) tag)
-    let tag_path = do_not_tag ()
-    let tag_ref = do_not_tag ()
-    let tag_var = do_not_tag ()
-  end)
-
-end
-
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 0241633c6..a0106837a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -11,11 +11,85 @@
 
 (** The default pretty-printers produce {!Pp.std_ppcmds} that are
     interpreted as raw strings. *)
-include Ppconstrsig.Pp
+open Loc
+open Pp
+open Libnames
+open Constrexpr
+open Names
+open Misctypes
 
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as annotated strings. The annotations can be
-    retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}. *)
+val extract_lam_binders :
+  constr_expr -> local_binder list * constr_expr
+val extract_prod_binders :
+  constr_expr -> local_binder list * constr_expr
+val split_fix :
+  int -> constr_expr -> constr_expr ->
+  local_binder list *  constr_expr * constr_expr
 
-module Richpp : Ppconstrsig.Pp
+val prec_less : int -> int * Ppextend.parenRelation -> bool
+
+val pr_tight_coma : unit -> std_ppcmds
+
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+
+val pr_lident : Id.t located -> std_ppcmds
+val pr_lname : Name.t located -> std_ppcmds
+
+val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
+val pr_com_at : int -> std_ppcmds
+val pr_sep_com :
+  (unit -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) ->
+  constr_expr -> std_ppcmds
+
+val pr_id : Id.t -> std_ppcmds
+val pr_name : Name.t -> std_ppcmds
+val pr_qualid : qualid -> std_ppcmds
+val pr_patvar : patvar -> std_ppcmds
+
+val pr_glob_level : glob_level -> std_ppcmds
+val pr_glob_sort : glob_sort -> std_ppcmds
+val pr_guard_annot : (constr_expr -> std_ppcmds) ->
+  local_binder list ->
+  ('a * Names.Id.t) option * recursion_order_expr ->
+  std_ppcmds
+
+val pr_record_body : (reference * constr_expr) list -> std_ppcmds
+val pr_binders : local_binder list -> std_ppcmds
+val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_constr_expr : constr_expr -> std_ppcmds
+val pr_lconstr_expr : constr_expr -> std_ppcmds
+val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
+
+type term_pr = {
+  pr_constr_expr   : constr_expr -> std_ppcmds;
+  pr_lconstr_expr  : constr_expr -> std_ppcmds;
+  pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+  pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+}
+
+val set_term_pr : term_pr -> unit
+val default_term_pr : term_pr
+
+(* The modular constr printer.
+  [modular_constr_pr pr s p t] prints the head of the term [t] and calls
+  [pr] on its subterms.
+  [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers
+  and [ltop] for "lconstr" printers (spiwack: we might need more
+  specification here).
+  We can make a new modular constr printer by overriding certain branches,
+  for instance if we want to build a printer which prints "Prop" as "Omega"
+  instead we can proceed as follows:
+  let my_modular_constr_pr pr s p = function
+  | CSort (_,GProp Null) -> str "Omega"
+  | t -> modular_constr_pr pr s p t
+  Which has the same type. We can turn a modular printer into a printer by
+  taking its fixpoint. *)
+
+type precedence
+val lsimpleconstr : precedence
+val ltop : precedence
+val modular_constr_pr :
+  ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
+  (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
deleted file mode 100644
index 3de0d805c..000000000
--- a/printing/ppconstrsig.mli
+++ /dev/null
@@ -1,95 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Loc
-open Pp
-open Libnames
-open Constrexpr
-open Names
-open Misctypes
-
-module type Pp = sig
-
-  val extract_lam_binders :
-    constr_expr -> local_binder list * constr_expr
-  val extract_prod_binders :
-    constr_expr -> local_binder list * constr_expr
-  val split_fix :
-    int -> constr_expr -> constr_expr ->
-    local_binder list *  constr_expr * constr_expr
-
-  val prec_less : int -> int * Ppextend.parenRelation -> bool
-
-  val pr_tight_coma : unit -> std_ppcmds
-
-  val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-
-  val pr_lident : Id.t located -> std_ppcmds
-  val pr_lname : Name.t located -> std_ppcmds
-
-  val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
-  val pr_com_at : int -> std_ppcmds
-  val pr_sep_com :
-    (unit -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) ->
-    constr_expr -> std_ppcmds
-
-  val pr_id : Id.t -> std_ppcmds
-  val pr_name : Name.t -> std_ppcmds
-  val pr_qualid : qualid -> std_ppcmds
-  val pr_patvar : patvar -> std_ppcmds
-
-  val pr_glob_level : glob_level -> std_ppcmds
-  val pr_glob_sort : glob_sort -> std_ppcmds
-  val pr_guard_annot : (constr_expr -> std_ppcmds) ->
-    local_binder list ->
-    ('a * Names.Id.t) option * recursion_order_expr ->
-    std_ppcmds
-
-  val pr_record_body : (reference * constr_expr) list -> std_ppcmds
-  val pr_binders : local_binder list -> std_ppcmds
-  val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
-  val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
-  val pr_constr_expr : constr_expr -> std_ppcmds
-  val pr_lconstr_expr : constr_expr -> std_ppcmds
-  val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
-
-  type term_pr = {
-    pr_constr_expr   : constr_expr -> std_ppcmds;
-    pr_lconstr_expr  : constr_expr -> std_ppcmds;
-    pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
-    pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
-  }
-
-  val set_term_pr : term_pr -> unit
-  val default_term_pr : term_pr
-
-(** The modular constr printer.
-    [modular_constr_pr pr s p t] prints the head of the term [t] and calls
-    [pr] on its subterms.
-    [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers
-    and [ltop] for "lconstr" printers (spiwack: we might need more
-    specification here).
-    We can make a new modular constr printer by overriding certain branches,
-    for instance if we want to build a printer which prints "Prop" as "Omega"
-    instead we can proceed as follows:
-    let my_modular_constr_pr pr s p = function
-    | CSort (_,GProp Null) -> str "Omega"
-    | t -> modular_constr_pr pr s p t
-    Which has the same type. We can turn a modular printer into a printer by
-    taking its fixpoint. *)
-
-  type precedence
-  val lsimpleconstr : precedence
-  val ltop : precedence
-  val modular_constr_pr :
-    ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
-    (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds
-
-end
-
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ff72be90c..78ef4d4ba 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -19,17 +19,12 @@ open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
 
-module Make
-  (Ppconstr : Ppconstrsig.Pp)
-  (Taggers  : sig
-    val tag_keyword : std_ppcmds -> std_ppcmds
-    val tag_vernac  : vernac_expr -> std_ppcmds -> std_ppcmds
-  end)
-= struct
-
-  open Taggers
   open Ppconstr
 
+  let do_not_tag _ x = x
+  let tag_keyword = do_not_tag ()
+  let tag_vernac  = do_not_tag
+
   let keyword s = tag_keyword (str s)
 
   let pr_constr = pr_constr_expr
@@ -526,7 +521,7 @@ module Make
   let pr_using e = str (Proof_using.to_string e)
 
   let rec pr_vernac_body v =
-    let return = Taggers.tag_vernac v in
+    let return = tag_vernac v in
     match v with
       | VernacPolymorphic (poly, v) ->
         let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
@@ -1244,23 +1239,3 @@ module Make
   let pr_vernac v =
     try pr_vernac_body v ++ sep_end v
     with e -> CErrors.print e
-
-end
-
-include Make (Ppconstr) (struct
-  let do_not_tag _ x = x
-  let tag_keyword = do_not_tag ()
-  let tag_vernac  = do_not_tag
-end)
-
-module Richpp = struct
-
-  include Make
-    (Ppconstr.Richpp)
-    (struct
-      open Ppannotation
-      let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s
-      let tag_vernac v s = Pp.tag (Pp.Tag.inj (AVernac v) tag) s
-     end)
-
-end
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index d3d4a5ceb..836b05e0e 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,12 +9,11 @@
 (** This module implements pretty-printers for vernac_expr syntactic
     objects and their subcomponents. *)
 
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as raw strings. *)
-include Ppvernacsig.Pp
+(** Prints a fixpoint body *)
+val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
 
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as annotated strings. The annotations can be
-    retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}. *)
-module Richpp : Ppvernacsig.Pp
+(** Prints a vernac expression *)
+val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
+
+(** Prints a vernac expression and closes it with a dot. *)
+val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
diff --git a/printing/printer.ml b/printing/printer.ml
index 00c2b636b..5e7e9ce54 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -722,7 +722,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
               (let s = Proof_global.Bullet.suggest p in
-               if Pp.is_empty s then s else fnl () ++ s) ++
+               if Pp.ismt s then s else fnl () ++ s) ++
               fnl ()
             in
 	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
diff --git a/printing/printing.mllib b/printing/printing.mllib
index b0141b6d3..86b68d8fb 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,6 +1,5 @@
 Genprint
 Pputils
-Ppannotation
 Ppconstr
 Printer
 Printmod
diff --git a/printing/printmod.ml b/printing/printmod.ml
index dfa66d437..baa1b8d79 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -26,6 +26,18 @@ open Goptions
     the "short" mode or (Some env) in the "rich" one.
 *)
 
+module Tag =
+struct
+
+  let definition = "module.definition"
+  let keyword    = "module.keyword"
+
+end
+
+let tag t s = Pp.tag t s
+let tag_definition s = tag Tag.definition s
+let tag_keyword s = tag Tag.keyword s
+
 let short = ref false
 
 let _ =
@@ -44,14 +56,8 @@ let mk_fake_top =
   let r = ref 0 in
   fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r))
 
-module Make (Taggers : sig
-  val tag_definition : std_ppcmds -> std_ppcmds
-  val tag_keyword : std_ppcmds -> std_ppcmds
-end) =
-struct
-
-let def s = Taggers.tag_definition (str s)
-let keyword s = Taggers.tag_keyword (str s)
+let def s = tag_definition (str s)
+let keyword s = tag_keyword (str s)
 
 let get_new_id locals id =
   let rec get_id l id =
@@ -397,11 +403,11 @@ let rec printable_body dir =
 
 let print_expression' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me
+    (fun e -> print_expression is_type env mp [] e) me
 
 let print_signature' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me
+    (fun e -> print_signature is_type env mp [] e) me
 
 let unsafe_print_module env mp with_body mb =
   let name = print_modpath [] mp in
@@ -441,20 +447,4 @@ let print_modtype kn =
       with e when CErrors.noncritical e ->
 	print_signature' true None kn mtb.mod_type))
 
-end
-
-module Tag =
-struct
-  let definition =
-    let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in
-    Ppstyle.make ~style ["module"; "definition"]
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["module"; "keyword"]
-end
 
-include Make(struct
-  let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
-  let tag_definition s = tag Tag.definition s
-  let tag_keyword s = tag Tag.keyword s
-end)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 7f7d34392..f3079d5b6 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -6,9 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Names
 
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-include Printmodsig.Pp
+val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
+val print_module : bool -> module_path -> std_ppcmds
+val print_modtype : module_path -> std_ppcmds
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 120cde5e5..ca7330fdb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -195,9 +195,9 @@ let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    CErrors.error (Pp.string_of_ppcmds
+    CErrors.user_err
       (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
-       str"Use \"Abort All\" first or complete proof(s)."))
+       str"Use \"Abort All\" first or complete proof(s).")
   end
 
 let discard_gen id =
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index a125fb10d..f51586c73 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids =
 let suggest_Proof_using name env vars ids_typ context_ids =
   let module S = Id.Set in
   let open Pp in
-  let print x = prerr_endline (string_of_ppcmds x) in
+  let print x = Feedback.msg_error x in
   let pr_set parens s =
     let wrap ppcmds =
       if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 8acc3c233..125491988 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -10,9 +10,9 @@ open CErrors
 open Pp
 open Util
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp
 
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
 
 type 'a worker_status = [ `Fresh | `Old of 'a ]
 
@@ -147,23 +147,23 @@ module Make(T : Task) = struct
     let stop_waiting = ref false in
     let expiration_date = ref (ref false) in
     let pick_task () =
-      prerr_endline "waiting for a task";
+      stm_prerr_endline "waiting for a task";
       let pick age (t, c) = not !c && T.task_match age t in
       let task, task_expiration =
         TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in
       expiration_date := task_expiration;
       last_task := Some task;
-      prerr_endline ("got task: "^T.name_of_task task);
+      stm_prerr_endline ("got task: " ^ T.name_of_task task);
       task in
     let add_tasks l =
       List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in
     let get_exec_token () =
       ignore(CoqworkmgrApi.get 1);
       got_token := true;
-      prerr_endline ("got execution token") in
+      stm_prerr_endline ("got execution token") in
     let kill proc =
       Worker.kill proc;
-      prerr_endline ("Worker exited: " ^
+      stm_prerr_endline ("Worker exited: " ^
         match Worker.wait proc with
         | Unix.WEXITED 0x400 -> "exit code unavailable"
         | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
@@ -196,7 +196,7 @@ module Make(T : Task) = struct
       report_status ~id "Idle";
       let task = pick_task () in
       match T.request_of_task !worker_age task with
-      | None -> prerr_endline ("Task expired: " ^ T.name_of_task task)
+      | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task)
       | Some req ->
       try
         get_exec_token ();
@@ -222,8 +222,7 @@ module Make(T : Task) = struct
           raise e (* we pass the exception to the external handler *)
       | MarshalError s -> T.on_marshal_error s task; raise Die
       | e ->
-          pr_err ("Uncaught exception in worker manager: "^
-            string_of_ppcmds (print e));
+          stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]);
           flush_all (); raise Die
     done with
     | (Die | TQueue.BeingDestroyed) ->
@@ -261,7 +260,7 @@ module Make(T : Task) = struct
   let broadcast { queue } = TQueue.broadcast queue
 
   let enqueue_task { queue; active } (t, _ as item) =
-    prerr_endline ("Enqueue task "^T.name_of_task t);
+    stm_prerr_endline ("Enqueue task "^T.name_of_task t);
     TQueue.push queue item
 
   let cancel_worker { active } n = Pool.cancel n active
@@ -298,18 +297,11 @@ module Make(T : Task) = struct
   let slave_handshake () =
     Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
 
-  let pp_pid pp = 
-    (* Breaking all abstraction barriers... very nice *)
-    let get_xml pp = match Richpp.repr pp with
-      | Xml_datatype.Element("_", [], xml) -> xml
-      | _ -> assert false in
-    Richpp.richpp_of_xml (Xml_datatype.Element("_", [],
-      get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @
-      get_xml pp))
+  let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp)
 
   let debug_with_pid = Feedback.(function
     | { contents = Message(Debug, loc, pp) } as fb ->
-       { fb with contents = Message(Debug,loc,pp_pid pp) }
+       { fb with contents = Message(Debug,loc, pp_pid pp) }
     | x -> x)
 
   let main_loop () =
@@ -317,7 +309,6 @@ module Make(T : Task) = struct
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
     Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
-    Feedback.set_logger Feedback.feedback_logger;
     (* We ask master to allocate universe identifiers *)
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
@@ -337,11 +328,11 @@ module Make(T : Task) = struct
         CEphemeron.clear ()
       with
       | MarshalError s ->
-        pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+        stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
       | End_of_file ->
-        prerr_endline "connection lost"; flush_all (); exit 2
+        stm_prerr_endline "connection lost"; flush_all (); exit 2
       | e ->
-        pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+        stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]);
         flush_all (); exit 1
     done
 
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 23538a467..0d2f9cb74 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -8,11 +8,7 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
 let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index fff6d5543..9d3047373 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -8,11 +8,7 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
 let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e56db4090..b9dbb7891 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,14 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err s  = Printf.eprintf "%s] %s\n"     (System.process_id ()) s; flush stderr
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr
 
-let prerr_endline s = if false then begin pr_err (s ()) end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
+let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else ()
+let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
-(* Opening ppvernac below aliases Richpp, see PR#185 *)
-let pp_to_richpp  = Richpp.richpp_of_pp
-let str_to_richpp = Richpp.richpp_of_string
+let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else ()
 
 open Vernacexpr
 open CErrors
@@ -26,7 +25,7 @@ open Feedback
 
 let execution_error state_id loc msg =
     feedback ~id:(State state_id)
-      (Message (Error, Some loc, pp_to_richpp msg))
+      (Message (Error, Some loc, msg))
 
 module Hooks = struct
 
@@ -48,7 +47,7 @@ let forward_feedback, forward_feedback_hook =
 
 let parse_error, parse_error_hook = Hook.make
  ~default:(fun id loc msg ->
-        feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) ()
+        feedback ~id (Message(Error, Some loc, msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
@@ -544,7 +543,7 @@ end = struct (* {{{ *)
         let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
           | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
         checkout branch;
-        prerr_endline (fun () -> "mode:" ^ mode);
+        stm_prerr_endline (fun () -> "mode:" ^ mode);
         Proof_global.activate_proof_mode mode
       with Failure _ ->
         checkout Branch.master;
@@ -856,7 +855,7 @@ end = struct (* {{{ *)
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
     try
-      prerr_endline (fun () -> "defining "^str_id^" (cache="^
+      stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
       let good_id = match safe_id with None -> !cur_id | Some id -> id in
       fix_exn_ref := exn_on id ~valid:good_id;
@@ -864,7 +863,7 @@ end = struct (* {{{ *)
       fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
-      prerr_endline (fun () -> "setting cur id to "^str_id);
+      stm_prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
       if feedback_processed then
         Hooks.(call state_computed id ~in_cache:false);
@@ -998,11 +997,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
   in
   let aux_interp cmd =
   if is_filtered_command cmd then
-    prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
+    stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr)
   else match cmd with
   | VernacShow ShowScript -> ShowScript.show_script ()
   | expr ->
-    prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
+    stm_pperr_endline Pp.(fun () -> str "interpreting " ++ pr_vernac expr);
     try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
     with e ->
       let e = CErrors.push e in
@@ -1435,11 +1434,10 @@ end = struct (* {{{ *)
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
         let e_msg = iprint (e, info) in
-        prerr_endline (fun () -> "failed with the following exception:");
-        prerr_endline (fun () -> string_of_ppcmds e_msg);
+        stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg);
         let e_safe_states = List.filter State.is_cached_and_valid my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
-  
+
   let perform_states query =
     if query = [] then [] else
     let is_tac e = match classify_vernac e with
@@ -1701,7 +1699,7 @@ end = struct (* {{{ *)
              | Some (ReqBuildProof (r, b, _)) -> Some(r, b)
              | _ -> None)
         tasks in
-    prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+    stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
     reqs
 
   let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1785,7 +1783,7 @@ end = struct (* {{{ *)
         `Stay ((),[])
                     
   let on_marshal_error err { t_name } =
-    pr_err ("Fatal marshal error: " ^ t_name );
+    stm_pr_err ("Fatal marshal error: " ^ t_name );
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death = function
@@ -1884,10 +1882,10 @@ end = struct (* {{{ *)
           let open Notations in
           try
             let pt, uc = Future.join f in
-            prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+            stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
-              str"uc=" ++ Evd.pr_evar_universe_context uc)));
+              str"uc=" ++ Evd.pr_evar_universe_context uc));
             (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
               (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
               Tactics.exact_no_check pt)
@@ -1929,7 +1927,7 @@ end = struct (* {{{ *)
   let use_response _ _ _ = `End
 
   let on_marshal_error _ _ =
-    pr_err ("Fatal marshal error in query");
+    stm_pr_err ("Fatal marshal error in query");
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death _ = ()
@@ -1945,7 +1943,7 @@ end = struct (* {{{ *)
       feedback ~id:(State r_for) Processed
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
-      let msg = pp_to_richpp (iprint e) in
+      let msg = iprint e     in
       feedback ~id:(State r_for) (Message (Error, None, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
@@ -2004,7 +2002,7 @@ let warn_deprecated_nested_proofs =
                     "stop working in a future Coq version"))
 
 let collect_proof keep cur hd brkind id =
- prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
  let name = function
    | [] -> no_name
@@ -2104,7 +2102,7 @@ let string_of_reason = function
   | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
   | `Unknown -> "unsupported case"
 
-let log_string s = prerr_debug (fun () -> "STM: " ^ s)
+let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s)
 let log_processing_async id name = log_string Printf.(sprintf
   "%s: proof %s: asynch" (Stateid.to_string id) name
 )
@@ -2191,16 +2189,16 @@ let known_state ?(redefine_qed=false) ~cache id =
     Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
   in
   let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
-    prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+    stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
     reach ~safe_id id;
     cherry_pick_non_pstate ()) id
 
   (* traverses the dag backward from nodes being already calculated *)
   and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
-    prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
+    stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached ~cache id then begin
       Hooks.(call state_computed id ~in_cache:true);
-      prerr_endline (fun () -> "reached (cache)");
+      stm_prerr_endline (fun () -> "reached (cache)");
       State.install_cached id
     end else
     let step, cache_step, feedback_processed =
@@ -2352,7 +2350,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       else cache_step in
     State.define ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
-    prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
+    stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
 end (* }}} *)
@@ -2367,7 +2365,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline (fun () -> "Initializing workers");
+    stm_prerr_endline (fun () -> "Initializing workers");
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
@@ -2419,9 +2417,9 @@ let rec join_admitted_proofs id =
 let join () =
   finish ();
   wait ();
-  prerr_endline (fun () -> "Joining the environment");
+  stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
-  prerr_endline (fun () -> "Joining Admitted proofs");
+  stm_prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
   VCS.print ()
@@ -2495,7 +2493,7 @@ let handle_failure (e, info) vcs tty =
       anomaly(str"error with no safe_id attached:" ++ spc() ++
         CErrors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
-      prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+      stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
       if tty && interactive () = `Yes then begin
         (* We stay on a valid state *)
@@ -2518,13 +2516,13 @@ let reset_task_queue = Slaves.reset_task_queue
 (* Document building *)
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty
   ({ verbose; loc; expr } as x) c =
-  prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
   try
     let head = VCS.current_branch () in
     VCS.checkout head;
     let rc = begin
-      prerr_endline (fun () ->
+      stm_prerr_endline (fun () ->
         "  classified as: " ^ string_of_vernac_classification c);
       match c with
       (* PG stuff *)    
@@ -2562,7 +2560,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
-          prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
+          stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2712,7 +2710,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
               expr = VernacShow (ShowGoal OpenSubgoals) }
       | _ -> ()
     end;
-    prerr_endline (fun () -> "processed }}}");
+    stm_prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
   with e ->
@@ -2898,7 +2896,7 @@ let edit_at id =
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
           CErrors.print_no_report e)
     | Some (_, id) ->
-        prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+        stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
         iraise (e, info)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 4b254e811..72b538016 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -5,6 +5,7 @@ TQueue
 WorkerPool
 Vernac_classifier
 CoqworkmgrApi
+WorkerLoop
 AsyncTaskQueue
 Stm
 ProofBlockDelimiter
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index d5333d107..256532c6b 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -8,11 +8,7 @@
 
 module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
 
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        W.init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
+let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
 
 let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/printing/ppvernacsig.mli b/stm/workerLoop.ml
index 5e5e4bcf4..50b42512c 100644
--- a/printing/ppvernacsig.mli
+++ b/stm/workerLoop.ml
@@ -6,15 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module type Pp = sig
+let rec parse = function
+  | "--xml_format=Ppcmds" :: rest -> parse rest
+  | x :: rest -> x :: parse rest
+  | [] -> []
 
-  (** Prints a fixpoint body *)
-  val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
-
-  (** Prints a vernac expression *)
-  val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
-
-  (** Prints a vernac expression and closes it with a dot. *)
-  val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
-
-end
+let loop init args =
+  let args = parse args in
+  Flags.make_silent true;
+  init ();
+  CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+  args
diff --git a/printing/printmodsig.mli b/stm/workerLoop.mli
index f71fffdce..dcbf9c88d 100644
--- a/printing/printmodsig.mli
+++ b/stm/workerLoop.mli
@@ -6,12 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Names
-
-module type Pp =
-sig
-  val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
-  val print_module : bool -> module_path -> std_ppcmds
-  val print_modtype : module_path -> std_ppcmds
-end
+val loop : (unit -> unit) -> string list -> string list
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index a2ee2d4c8..979396969 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -97,8 +97,8 @@ Expands to: Constant Top.f
 forall w : r, w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Unknown interpretation for notation "$".
+Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra arguments: _, _.
+Extra arguments: _, _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index b084ad498..4df21ae35 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,5 +1,5 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
@@ -103,15 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: Argument lists should agree on the names they provide.
+Argument lists should agree on the names they provide.
 The command has indeed failed with message:
-Error: Sequences of implicit arguments must be of different lengths.
+Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Some argument names are duplicated: F
+Some argument names are duplicated: F
 The command has indeed failed with message:
-Error: Argument z cannot be declared implicit.
+Argument z cannot be declared implicit.
 The command has indeed failed with message:
-Error: Extra arguments: y.
+Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 06a6b2d15..38d055b28 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
 Ltac call to "instantiate ( (ident) := (lglob) )" failed.
-Error: Instance is not well-typed in the environment of ?x.
+Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index c6786c72f..8d2a125c1 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -16,4 +16,4 @@ Tactic failure: Already an intensional equality.
 The command has indeed failed with message:
 In nested Ltac calls to "extensionality in (var)" and
 "clearbody (ne_var_list)", last call failed.
-Error: Hypothesis e depends on the body of H'
+Hypothesis e depends on the body of H'
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 26eaca827..9d106d2da 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0
 -4
      : Z
 The command has indeed failed with message:
-Error: x should not be bound in a recursive pattern of the right-hand side.
+x should not be bound in a recursive pattern of the right-hand side.
 The command has indeed failed with message:
-Error: in the right-hand side, y and z should appear in
+in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
 The reference w was not found in the current environment.
 The command has indeed failed with message:
-Error: in the right-hand side, y and z should appear in
+in the right-hand side, y and z should appear in
 term position as part of a recursive pattern.
 The command has indeed failed with message:
-Error: z is expected to occur in binding position in the right-hand side.
+z is expected to occur in binding position in the right-hand side.
 The command has indeed failed with message:
-Error: as y is a non-closed binder, no such "," is allowed to occur.
+as y is a non-closed binder, no such "," is allowed to occur.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Cannot find where the recursive pattern starts.
+Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
-Error: Both ends of the recursive pattern are the same.
+Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 1ff09e3af..35c3057d8 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,5 +1,4 @@
 The command has indeed failed with message:
-Error:
 Ltac variable y depends on pattern variable name z which is not bound in current context.
 Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
@@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 Hx
 nat
 nat
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
index ae3fd7acc..172612405 100644
--- a/test-suite/output/ltac_missing_args.out
+++ b/test-suite/output/ltac_missing_args.out
@@ -1,21 +1,20 @@
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable x.
+A fully applied tactic is expected: missing argument for variable x.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable x.
+A fully applied tactic is expected: missing argument for variable x.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected:
-missing arguments for variables y and _.
+A fully applied tactic is expected: missing arguments for variables y and _.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable x.
+A fully applied tactic is expected: missing argument for variable x.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable x.
+A fully applied tactic is expected: missing argument for variable x.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable _.
+A fully applied tactic is expected: missing argument for variable _.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable _.
+A fully applied tactic is expected: missing argument for variable _.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable _.
+A fully applied tactic is expected: missing argument for variable _.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable x.
+A fully applied tactic is expected: missing argument for variable x.
 The command has indeed failed with message:
-Error: A fully applied tactic is expected: missing argument for variable x.
+A fully applied tactic is expected: missing argument for variable x.
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 8fcca535d..932097607 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -12,24 +12,15 @@ let error s =
   prerr_endline ("fake_id: error: "^s);
   exit 1
 
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
 type coqtop = {
   xml_printer : Xml_printer.t;
   xml_parser : Xml_parser.t;
 }
 
-let print_xml chan xml =
-  let rec print = function
-  | Xml_datatype.PCData s -> output_string chan s
-  | Xml_datatype.Element (_, _, children) -> List.iter print children
-  in
-  print xml
-
-let error_xml s =
-  Printf.eprintf "fake_id: error: %a\n%!" print_xml s;
-  exit 1
-
-let logger level content =
-  Printf.eprintf "%a\n%! " print_xml (Richpp.repr content)
+let print_error msg =
+  Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -37,20 +28,15 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
-    match Xmlprotocol.is_message xml with
-    | Some (level, _loc, content) ->
-      logger level content;
+    if Xmlprotocol.is_feedback xml then
       loop ()
-    | None ->
-      if Xmlprotocol.is_feedback xml then
-        loop ()
-      else Xmlprotocol.to_answer call xml
+    else Xmlprotocol.to_answer call xml
   in
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);
   match res with
-  | Interface.Fail (_,_,s) when fail -> error_xml (Richpp.repr s)
-  | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); x
+  | Interface.Fail (_,_,s) when fail -> print_error s; exit 1
+  | Interface.Fail (_,_,s) as x      -> print_error s; x
   | x -> x
 
 let eval_call c q = ignore(base_eval_call c q)
@@ -186,7 +172,7 @@ let print_document () =
           Str.global_replace (Str.regexp "^[\n ]*") ""
       (if String.length s > 20 then String.sub s 0 17 ^ "..."
        else s) in
-  prerr_endline (Pp.string_of_ppcmds
+  pperr_endline (
     (Document.print doc
       (fun b state_id { name; text } ->
         Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
@@ -199,7 +185,7 @@ let print_document () =
 module GUILogic = struct
 
   let after_add = function
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+    | Interface.Fail (_,_,s) -> print_error s; exit 1
     | Interface.Good (id, (Util.Inl (), _)) ->
         Document.assign_tip_id doc id
     | Interface.Good (id, (Util.Inr tip, _)) ->
@@ -211,7 +197,7 @@ module GUILogic = struct
   let at id id' _ = Stateid.equal id' id
   
   let after_edit_at (id,need_unfocus) = function
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+    | Interface.Fail (_,_,s) -> print_error s; exit 1
     | Interface.Good (Util.Inl ()) ->
         if need_unfocus then Document.unfocus doc;
         ignore(Document.cut_at doc id);
@@ -310,11 +296,12 @@ let main =
   Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
+  let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
   let coqtop_name, coqtop_args, input_file = match Sys.argv with
-    | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+    | [| _; f |] -> "coqtop", Array.of_list def_args, f
     | [| _; f; ct |] ->
         let ct = Str.split (Str.regexp " ") ct in
-        List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
+        List.hd ct, Array.of_list (def_args @ List.tl ct), f
     | _ -> usage () in
   let inc = if input_file = "-" then stdin else open_in input_file in
   let coq =
@@ -334,7 +321,7 @@ let main =
   let finish () =
     match base_eval_call (Xmlprotocol.status true) coq with
     | Interface.Good _ -> exit 0
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in
+    | Interface.Fail (_,_,s) -> print_error s; exit 1 in
   (* The main loop *)
   init ();
   while true do
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 0dfd06726..0cc6ca317 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,7 +13,8 @@ open Flags
 open Vernac
 open Pcoq
 
-let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x
+let top_stderr x =
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x
 
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
@@ -251,7 +252,8 @@ let print_toplevel_error (e, info) =
       else mt ()
     else print_location_in_file loc
   in
-  locmsg ++ CErrors.iprint (e, info)
+  let hdr msg = hov 0 (Topfmt.err_hdr ++ msg) in
+  locmsg ++ hdr (CErrors.iprint (e, info))
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =
@@ -283,6 +285,33 @@ let read_sentence input =
     discard_to_dot ();
     iraise reraise
 
+(** Coqloop Console feedback handler *)
+let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
+  match fb.contents with
+  | Processed   -> ()
+  | Incomplete  -> ()
+  | Complete    -> ()
+  | ProcessingIn _ -> ()
+  | InProgress _ -> ()
+  | WorkerStatus (_,_) -> ()
+  | AddedAxiom  -> ()
+  | GlobRef (_,_,_,_,_) -> ()
+  | GlobDef (_,_,_,_) -> ()
+  | FileDependency (_,_) -> ()
+  | FileLoaded (_,_) -> ()
+  | Custom (_,_,_) -> ()
+  | Message (Error,loc,msg) ->
+    (* We ignore errors here as we (still) have a different error
+       printer for the toplevel. It is hard to solve due the many
+       error paths presents, and the different compromise of feedback
+       error forwaring in the stm depending on the mode *)
+    ()
+  | Message (lvl,loc,msg) ->
+    if !Flags.print_emacs then
+      Topfmt.emacs_logger ?loc lvl msg
+    else
+      Topfmt.std_logger ?loc lvl msg
+
 (** [do_vernac] reads and executes a toplevel phrase, and print error
     messages when an exception is raised, except for the following:
     - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
@@ -305,12 +334,13 @@ let do_vernac () =
         top_stderr (fnl ()); raise CErrors.Quit
     | CErrors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise CErrors.Drop
-        else Feedback.msg_error (str"There is no ML toplevel.")
+        else top_stderr (str "There is no ML toplevel.")
     | any ->
+        (** Main error printer, note that this didn't it the "emacs"
+            legacy path. *)
         let any = CErrors.push any in
         let msg = print_toplevel_error any ++ fnl () in
-        pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
-        Format.pp_print_flush !Pp_control.std_ft ()
+        top_stderr msg
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -318,22 +348,13 @@ let do_vernac () =
     exit the loop are Drop and Quit. Any other exception there indicates
     an issue with [print_toplevel_error] above. *)
 
-(*
-let feed_emacs = function
-  | { Interface.id = Interface.State id;
-      Interface.content = Interface.GlobRef (_,a,_,c,_) }  -> 
-    prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>"
-		   ^a^" "^c^ "</info>")
-  | _  -> ()
-*)
-
 (* Flush in a compatible order with 8.5 *)
 (* This mimics the semantics of the old Pp.flush_all *)
 let loop_flush_all () =
   Pervasives.flush stderr;
   Pervasives.flush stdout;
-  Format.pp_print_flush !Pp_control.std_ft ();
-  Format.pp_print_flush !Pp_control.err_ft ()
+  Format.pp_print_flush !Topfmt.std_ft ();
+  Format.pp_print_flush !Topfmt.err_ft ()
 
 let rec loop () =
   Sys.catch_break true;
@@ -346,9 +367,9 @@ let rec loop () =
     | CErrors.Drop -> ()
     | CErrors.Quit -> exit 0
     | any ->
-      Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
-                str (Printexc.to_string any) ++
-                fnl() ++
-                str"Please report" ++
-                strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
+      top_stderr (str"Anomaly: main loop exited with exception: " ++
+                  str (Printexc.to_string any) ++
+                  fnl() ++
+                  str"Please report" ++
+                  strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
       loop ()
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index d248f2f70..eb61084e0 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,6 +32,8 @@ val set_prompt : (unit -> string) -> unit
 
 val print_toplevel_error : Exninfo.iexn -> std_ppcmds
 
+val coqloop_feed : Feedback.feedback -> unit
+
 (** Parse and execute one vernac command. *)
 
 val do_vernac : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c9a1f0def..0cd5498fe 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -61,15 +61,15 @@ let init_color () =
     match colors with
     | None ->
       (** Default colors *)
-      Feedback.init_color_output ()
+      Topfmt.init_color_output ()
     | Some "" ->
       (** No color output *)
       ()
     | Some s ->
       (** Overwrite all colors *)
-      Ppstyle.clear_styles ();
-      Ppstyle.parse_config s;
-      Feedback.init_color_output ()
+      Topfmt.clear_styles ();
+      Topfmt.parse_color_config s;
+      Topfmt.init_color_output ()
   end
 
 let toploop_init = ref begin fun x ->
@@ -78,15 +78,27 @@ let toploop_init = ref begin fun x ->
   x
   end
 
-let toploop_run = ref (fun () ->
+(* Feedback received in the init stage, this is different as the STM
+   will not be generally be initialized, thus stateid, etc... may be
+   bogus. For now we just print to the console too *)
+let coqtop_init_feed = Coqloop.coqloop_feed
+
+(* Default toplevel loop *)
+let console_toploop_run () =
+  (* We initialize the console only if we run the toploop_run *)
+  let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
   if Dumpglob.dump () then begin
     if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
   Coqloop.loop();
+  (* We remove the feeder but it could be ok not to do so *)
+  Feedback.del_feeder tl_feed;
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
-  Mltop.ocaml_toploop())
+  Mltop.ocaml_toploop()
+
+let toploop_run = ref console_toploop_run
 
 let output_context = ref false
 
@@ -227,7 +239,6 @@ let compile_files () =
   if !compile_list == [] then ()
   else
     let init_state = States.freeze ~marshallable:`No in
-    Feedback.(add_feeder debug_feeder);
     List.iter (fun vf ->
         States.unfreeze init_state;
         compile_file vf)
@@ -239,7 +250,6 @@ let set_emacs () =
   if not (Option.is_empty !toploop) then
     error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
-  Feedback.(set_logger emacs_logger);
   Vernacentries.qed_display_script := false;
   color := `OFF
 
@@ -297,24 +307,16 @@ let usage () =
 
 let print_style_tags () =
   let () = init_color () in
-  let tags = Ppstyle.dump () in
+  let tags = Topfmt.dump_tags () in
   let iter (t, st) =
-    let st = match st with Some st -> st | None -> Terminal.make () in
-    let opt =
-      Terminal.eval st ^
-      String.concat "." (Ppstyle.repr t) ^
-      Terminal.reset ^ "\n"
-    in
+    let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in
     print_string opt
   in
-  let make (t, st) = match st with
-  | None -> None
-  | Some st ->
+  let make (t, st) =
     let tags = List.map string_of_int (Terminal.repr st) in
-    let t = String.concat "." (Ppstyle.repr t) in
-    Some (t ^ "=" ^ String.concat ";" tags)
+    (t ^ "=" ^ String.concat ";" tags)
   in
-  let repr = List.map_filter make tags in
+  let repr = List.map make tags in
   let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in
   let () = List.iter iter tags in
   flush_all ()
@@ -430,6 +432,13 @@ let get_native_name s =
       Nativelib.output_dir; Library.native_name_from_filename s]
   with _ -> ""
 
+(** Prints info which is either an error or an anomaly and then exits
+    with the appropriate error code *)
+let fatal_error info anomaly =
+  let msg = info ++ fnl () in
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
+  exit (if anomaly then 129 else 1)
+
 let parse_args arglist =
   let args = ref arglist in
   let extras = ref [] in
@@ -593,13 +602,14 @@ let parse_args arglist =
     parse ()
   with
     | UserError(_, s) as e ->
-      if is_empty s then exit 1
+      if ismt s then exit 1
       else fatal_error (CErrors.print e) false
     | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any)
 
 let init_toplevel arglist =
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+  let init_feeder = Feedback.add_feeder coqtop_init_feed in
   Lib.init();
   begin
     try
@@ -654,7 +664,8 @@ let init_toplevel arglist =
       Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
     Profile.print_profile ();
     exit 0
-  end
+  end;
+  Feedback.del_feeder init_feeder
 
 let start () =
   let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b73321c00..06908abb6 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -143,7 +143,8 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
       | None -> mt() in
     let after = comment (CLexer.extract_comments (snd loc)) in
     if !beautify_file then
-      Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
+      (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after));
+       Format.pp_print_flush !Topfmt.std_ft ())
     else
       Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
     States.unfreeze fs;
@@ -178,9 +179,10 @@ let pp_cmd_header loc com =
 (* This is a special case where we assume we are in console batch mode
    and take control of the console.
  *)
+(* FIXME *)
 let print_cmd_header loc com =
-  Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com);
-  Format.pp_print_flush !Pp_control.std_ft ()
+  Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com);
+  Format.pp_print_flush !Topfmt.std_ft ()
 
 let rec interp_vernac po chan_beautify checknav (loc,com) =
   let interp = function
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 594f2e944..6d71601cc 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -444,14 +444,14 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                with Not_found ->
 		 (* spiwack: the format of this error message should probably
 	                     be improved. *)
-		 let err_msg = string_of_ppcmds
+		 let err_msg =
 	                                (str "boolean->Leibniz:" ++
                                          str "You have to declare the" ++
 			   	         str "decidability over " ++
 				         Printer.pr_constr tt1 ++
 				         str " first.")
 		 in
-		 error err_msg
+		 user_err err_msg
                in let bl_args =
                         Array.append (Array.append
                           (Array.map (fun x -> x) v)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 17897460c..f1e0c48f0 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -45,15 +45,9 @@ let _ = CErrors.register_handler explain_exn_default
 
 (** Pre-explain a vernac interpretation error *)
 
-let wrap_vernac_error with_header (exn, info) strm =
-  if with_header then
-    let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
-    let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
-    (e, info)
-  else
-    (EvaluatedError (strm, None), info)
+let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info)
 
-let process_vernac_interp_error with_header exn = match fst exn with
+let process_vernac_interp_error exn = match fst exn with
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
@@ -61,40 +55,40 @@ let process_vernac_interp_error with_header exn = match fst exn with
 	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
       else
 	mt() in
-    wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".")
+    wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te)
+      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te)
+      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te)
+      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_inductive_error e)
+      wrap_vernac_error exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_module_error e)
+      wrap_vernac_error exn (Himsg.explain_module_error e)
   | Modintern.ModuleInternalizationError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e)
+      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
   | RecursionSchemeError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e)
+      wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,sigma,e) ->
-      wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e)
+      wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
   | Tacred.ReductionTacticError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e)
+      wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error with_header exn (Himsg.explain_refiner_error e)
+      wrap_vernac_error exn (Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
-      wrap_vernac_error with_header exn
+      wrap_vernac_error exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	 spc () ++ str "was not found" ++
 	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Refiner.FailError (i,s) ->
       let s = Lazy.force s in
-      wrap_vernac_error with_header exn
+      wrap_vernac_error exn
 	(str "Tactic failure" ++
-         (if Pp.is_empty s then s else str ": " ++ s) ++
+         (if Pp.ismt s then s else str ": " ++ s) ++
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
-      wrap_vernac_error with_header exn (msg ++ str ".")
+      wrap_vernac_error exn (msg ++ str ".")
   | _ ->
       exn
 
@@ -108,9 +102,9 @@ let additional_error_info = ref []
 let register_additional_error_info f =
   additional_error_info := f :: !additional_error_info
 
-let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
+let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error with_header (exc, info) in
+  let e = process_vernac_interp_error (exc, info) in
   let () =
     if not allow_uncaught && not (CErrors.handled (fst e)) then
       let (e, info) = e in
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index a67c887af..370ad7e3b 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -11,7 +11,7 @@ exception EvaluatedError of Pp.std_ppcmds * exn option
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/vernac/search.ml b/vernac/search.ml
index e1b56b131..540573843 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -367,7 +367,7 @@ let interface_search =
     let answer = {
       coq_object_prefix = prefix;
       coq_object_qualid = qualid;
-      coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr);
+      coq_object_object = constr;
     } in
     ans := answer :: !ans;
   in
diff --git a/vernac/search.mli b/vernac/search.mli
index c9167c485..82b79f75d 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -67,7 +67,7 @@ type 'a coq_object = {
 }
 
 val interface_search : ?glnum:int -> (search_constraint * bool) list ->
-  string coq_object list
+  constr coq_object list
 
 (** {6 Generic search function} *)
 
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
new file mode 100644
index 000000000..f843484f7
--- /dev/null
+++ b/vernac/topfmt.ml
@@ -0,0 +1,289 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Feedback
+open Pp
+
+(** Pp control also belongs here as the terminal is private to the toplevel *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+(* Default parameters of pretty-printing *)
+
+let dflt_gp = {
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 50;
+  ellipsis   = "..." }
+
+(* A deeper pretty-printer to print proof scripts *)
+
+let deep_gp = {
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 10000;
+  ellipsis   = "..." }
+
+(* set_gp : Format.formatter -> pp_global_params -> unit
+ * set the parameters of a formatter *)
+
+let set_gp ft gp =
+  Format.pp_set_margin ft gp.margin ;
+  Format.pp_set_max_indent ft gp.max_indent ;
+  Format.pp_set_max_boxes ft gp.max_depth ;
+  Format.pp_set_ellipsis_text ft gp.ellipsis
+
+let set_dflt_gp ft = set_gp ft dflt_gp
+
+let get_gp ft =
+  { margin = Format.pp_get_margin ft ();
+    max_indent = Format.pp_get_max_indent ft ();
+    max_depth = Format.pp_get_max_boxes ft ();
+    ellipsis = Format.pp_get_ellipsis_text ft () }
+
+(* with_fp : 'a pp_formatter_params -> Format.formatter
+ * returns of formatter for given formatter functions *)
+
+let with_fp chan out_function flush_function =
+  let ft = Format.make_formatter out_function flush_function in
+  Format.pp_set_formatter_out_channel ft chan;
+  ft
+
+(* Output on a channel ch *)
+
+let with_output_to ch =
+  let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in
+  set_gp ft deep_gp;
+  ft
+
+let std_ft = ref Format.std_formatter
+let _ = set_dflt_gp !std_ft
+
+let err_ft = ref Format.err_formatter
+let _ = set_gp !err_ft deep_gp
+
+let deep_ft = ref (with_output_to stdout)
+let _ = set_gp !deep_ft deep_gp
+
+(* For parametrization through vernacular *)
+let default = Format.pp_get_max_boxes !std_ft ()
+let default_margin = Format.pp_get_margin !std_ft ()
+
+let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ())
+let set_depth_boxes v =
+  Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v)
+
+let get_margin () = Some (Format.pp_get_margin !std_ft ())
+let set_margin v =
+  let v = match v with None -> default_margin | Some v -> v in
+  Format.pp_set_margin Format.str_formatter v;
+  Format.pp_set_margin !std_ft v;
+  Format.pp_set_margin !deep_ft v;
+  (* Heuristic, based on usage: the column on the right of max_indent
+     column is 20% of width, capped to 30 characters *)
+  let m = max (64 * v / 100) (v-30) in
+  Format.pp_set_max_indent Format.str_formatter m;
+  Format.pp_set_max_indent !std_ft m;
+  Format.pp_set_max_indent !deep_ft m
+
+(** Console display of feedback *)
+
+(** Default tags *)
+module Tag = struct
+
+  let error   = "message.error"
+  let warning = "message.warning"
+  let debug   = "message.debug"
+
+end
+
+type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
+
+let msgnl_with fmt strm =
+  pp_with fmt (strm ++ fnl ());
+  Format.pp_print_flush fmt ()
+
+(* XXX: This is really painful! *)
+module Emacs = struct
+
+  (* Special chars for emacs, to detect warnings inside goal output *)
+  let emacs_quote_start = String.make 1 (Char.chr 254)
+  let emacs_quote_end   = String.make 1 (Char.chr 255)
+
+  let emacs_quote_err g =
+    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+
+  let emacs_quote_info_start = "<infomsg>"
+  let emacs_quote_info_end = "</infomsg>"
+
+  let emacs_quote_info g =
+    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+
+end
+
+open Emacs
+
+let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
+let info_hdr = mt ()
+let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
+let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
+
+let make_body quoter info ?loc s =
+  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+  quoter (hov 0 (loc ++ info ++ s))
+
+(* Generic logger *)
+let gen_logger dbg err ?loc level msg = match level with
+  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?loc msg)
+  | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg)
+  (* XXX: What to do with loc here? *)
+  | Notice  -> msgnl_with !std_ft msg
+  | Warning -> Flags.if_warn (fun () ->
+               msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?loc msg)
+
+(** Standard loggers *)
+
+(* We provide a generic clear_log_backend callback for backends
+   wanting to do clenaup after the print.
+*)
+let std_logger_cleanup = ref (fun () -> ())
+
+let std_logger ?loc level msg =
+  gen_logger (fun x -> x) (fun x -> x) ?loc level msg;
+  !std_logger_cleanup ()
+
+(** Color logging. Moved from Ppstyle, it may need some more refactoring  *)
+
+(* Tag map for terminal style *)
+let default_tag_map () = let open Terminal in [
+  (* Local to console toplevel *)
+    "message.error"    , make ~bold:true ~fg_color:`WHITE ~bg_color:`RED ()
+  ; "message.warning"  , make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW ()
+  ; "message.debug"    , make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA ()
+  (* Coming from the printer *)
+  ; "constr.evar"      , make            ~fg_color:`LIGHT_BLUE ()
+  ; "constr.keyword"   , make ~bold:true ()
+  ; "constr.type"      , make ~bold:true ~fg_color:`YELLOW ()
+  ; "constr.notation"  , make ~fg_color:`WHITE ()
+  (* ["constr"; "variable"] is not assigned *)
+  ; "constr.reference" , make ~fg_color:`LIGHT_GREEN ()
+  ; "constr.path"      , make ~fg_color:`LIGHT_MAGENTA ()
+  ; "module.definition", make ~bold:true ~fg_color:`LIGHT_RED ()
+  ; "module.keyword"   , make ~bold:true ()
+  ; "tactic.keyword"   , make ~bold:true ()
+  ; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN ()
+  ; "tactic.string"    , make ~fg_color:`LIGHT_RED ()
+  ]
+
+let tag_map = ref CString.Map.empty
+
+let init_tag_map styles =
+  let set accu (name, st) = CString.Map.add name st accu in
+  tag_map := List.fold_left set !tag_map styles
+
+let clear_styles () =
+  tag_map := CString.Map.empty
+
+let parse_color_config file =
+  let styles = Terminal.parse file in
+  init_tag_map styles
+
+let dump_tags () = CString.Map.bindings !tag_map
+
+(** Not thread-safe. We should put a lock somewhere if we print from
+    different threads. Do we? *)
+let make_style_stack () =
+  (** Default tag is to reset everything *)
+  let empty = Terminal.make () in
+  let default_tag = Terminal.({
+      fg_color = Some `DEFAULT;
+      bg_color = Some `DEFAULT;
+      bold = Some false;
+      italic = Some false;
+      underline = Some false;
+      negative = Some false;
+    })
+  in
+  let style_stack = ref [] in
+  let peek () = match !style_stack with
+  | []      -> default_tag  (** Anomalous case, but for robustness *)
+  | st :: _ -> st
+  in
+  let push tag =
+    let style =
+      try CString.Map.find tag !tag_map
+      with | Not_found -> empty
+    in
+    (** Use the merging of the latest tag and the one being currently pushed.
+    This may be useful if for instance the latest tag changes the background and
+    the current one the foreground, so that the two effects are additioned. *)
+    let style = Terminal.merge (peek ()) style in
+    style_stack := style :: !style_stack;
+    Terminal.eval style
+  in
+  let pop _ = match !style_stack with
+  | []       -> (** Something went wrong, we fallback *)
+                Terminal.eval default_tag
+  | _ :: rem -> style_stack := rem;
+                Terminal.eval (peek ())
+  in
+  let clear () = style_stack := [] in
+  push, pop, clear
+
+let init_color_output () =
+  init_tag_map (default_tag_map ());
+  let push_tag, pop_tag, clear_tag = make_style_stack () in
+  std_logger_cleanup := clear_tag;
+  let tag_handler = {
+    Format.mark_open_tag   = push_tag;
+    Format.mark_close_tag  = pop_tag;
+    Format.print_open_tag  = ignore;
+    Format.print_close_tag = ignore;
+  } in
+  Format.pp_set_mark_tags !std_ft true;
+  Format.pp_set_mark_tags !err_ft true;
+  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
+  Format.pp_set_formatter_tag_functions !err_ft tag_handler
+
+(* Rules for emacs:
+   - Debug/info: emacs_quote_info
+   - Warning/Error: emacs_quote_err
+   - Notice: unquoted
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+
+(* Output to file, used only in extraction so a candidate for removal *)
+let ft_logger old_logger ft ?loc level mesg =
+  let id x = x in
+  match level with
+  | Debug   -> msgnl_with ft (make_body id  dbg_hdr mesg)
+  | Info    -> msgnl_with ft (make_body id info_hdr mesg)
+  | Notice  -> msgnl_with ft mesg
+  | Warning -> old_logger ?loc level mesg
+  | Error   -> old_logger ?loc level mesg
+
+let with_output_to_file fname func input =
+  (* XXX FIXME: redirect std_ft  *)
+  (* let old_logger = !logger in *)
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *)
+  try
+    let output = func input in
+    (* logger := old_logger; *)
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    (* logger := old_logger; *)
+    close_out channel;
+    Exninfo.iraise reraise
diff --git a/lib/pp_control.mli b/vernac/topfmt.mli
index d26f89eb3..1555f80a9 100644
--- a/lib/pp_control.mli
+++ b/vernac/topfmt.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Parameters of pretty-printing. *)
+(** Console printing options *)
 
 type pp_global_params = {
   margin : int;
@@ -20,13 +20,12 @@ val set_gp : Format.formatter -> pp_global_params -> unit
 val set_dflt_gp : Format.formatter -> unit
 val get_gp : Format.formatter -> pp_global_params
 
-
 (** {6 Output functions of pretty-printing. } *)
 
 val with_output_to : out_channel -> Format.formatter
 
-val std_ft : Format.formatter ref
-val err_ft : Format.formatter ref
+val std_ft  : Format.formatter ref
+val err_ft  : Format.formatter ref
 val deep_ft : Format.formatter ref
 
 (** {6 For parametrization through vernacular. } *)
@@ -36,3 +35,21 @@ val get_depth_boxes : unit -> int option
 
 val set_margin : int option -> unit
 val get_margin : unit -> int option
+
+(** Headers for tagging *)
+val err_hdr : Pp.std_ppcmds
+
+(** Console display of feedback *)
+val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+
+val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+
+val init_color_output : unit -> unit
+val clear_styles : unit -> unit
+val parse_color_config : string -> unit
+val dump_tags : unit -> (string * Terminal.style) list
+
+(** [with_output_to_file file f x] executes [f x] with logging
+    redirected to a file [file] *)
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 94ef54f70..283c095eb 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -14,4 +14,5 @@ Record
 Assumptions
 Vernacinterp
 Mltop
+Topfmt
 Vernacentries
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3afe04b37..32e18a014 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -39,8 +39,9 @@ module NamedDecl = Context.Named.Declaration
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
-let prerr_endline x =
-  if debug then prerr_endline (x ()) else ()
+(* XXX Should move to a common library *)
+let vernac_pperr_endline pp =
+  if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
 
 (* Misc *)
 
@@ -1448,8 +1449,8 @@ let _ =
       optdepr  = false;
       optname  = "the printing depth";
       optkey   = ["Printing";"Depth"];
-      optread  = Pp_control.get_depth_boxes;
-      optwrite = Pp_control.set_depth_boxes }
+      optread  = Topfmt.get_depth_boxes;
+      optwrite = Topfmt.set_depth_boxes }
 
 let _ =
   declare_int_option
@@ -1457,8 +1458,8 @@ let _ =
       optdepr  = false;
       optname  = "the printing width";
       optkey   = ["Printing";"Width"];
-      optread  = Pp_control.get_margin;
-      optwrite = Pp_control.set_margin }
+      optread  = Topfmt.get_margin;
+      optwrite = Topfmt.set_margin }
 
 let _ =
   declare_bool_option
@@ -1933,7 +1934,7 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~loc locality poly c =
-  prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
   match c with
   (* The below vernac are candidates for removal from the main type
      and to be put into a new doc_command datatype: *)
@@ -2193,7 +2194,7 @@ let with_fail b f =
            | e ->
               let e = CErrors.push e in
               raise (HasFailed (CErrors.iprint
-                (ExplainErr.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e))))
+                (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))))
         ()
     with e when CErrors.noncritical e ->
       let (e, _) = CErrors.push e in
@@ -2226,7 +2227,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacRedirect (s, (_,v)) ->
-         Feedback.with_output_to_file s (aux false) v
+         Topfmt.with_output_to_file s (aux false) v
     | VernacTime (_,v) ->
         System.with_time !Flags.time
           (aux ?locality ?polymorphism isprogcmd) v;