Merge PR#390: Updates to the Pretty Printing Infrastructure

13 files changed, 156 insertions, 996 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index dbebe6a48f..99b763602d 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 5cffc725d9..0665a8ce73 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 1e33173ee1..c73ae9b904 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 57c6f30a41..7d9d6bf7f0 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 b4bed8793d..4bbdfcb5b6 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 a51b4458fb..9f33756dfe 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 f17908262c..802ffe8e7a 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 ab8dc0798c..0000000000
--- 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/pp_control.mli b/lib/pp_control.mli
deleted file mode 100644
index d26f89eb30..0000000000
--- a/lib/pp_control.mli
+++ /dev/null
@@ -1,38 +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 }
-
-val dflt_gp : pp_global_params
-val deep_gp : pp_global_params
-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 deep_ft : Format.formatter ref
-
-(** {6 For parametrization through vernacular. } *)
-
-val set_depth_boxes : int option -> unit
-val get_depth_boxes : unit -> int option
-
-val set_margin : int option -> unit
-val get_margin : unit -> int option
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
deleted file mode 100644
index aa47c51671..0000000000
--- 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 d9fd757656..0000000000
--- 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/lib/richpp.ml b/lib/richpp.ml
deleted file mode 100644
index d1c6d158e4..0000000000
--- a/lib/richpp.ml
+++ /dev/null
@@ -1,203 +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 Util
-open Xml_datatype
-
-type 'annotation located = {
-  annotation : 'annotation option;
-  startpos   : int;
-  endpos     : int
-}
-
-type 'a stack =
-| Leaf
-| Node of string * 'a located gxml list * int * 'a stack
-
-type 'a context = {
-  mutable stack : 'a stack;
-  (** 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.
-    Each inserted tag is a fresh index that we keep in sync with the contents
-    of annotations.
-
-    We build an XML tree on the fly, by plugging ourselves in Format tag
-    marking functions. As those functions are called when actually writing to
-    the device, the resulting tree is correct.
-*)
-let rich_pp annotate 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 () =
-    (** Push the optional PCData on the above node *)
-    let len = Buffer.length pp_buffer in
-    if len = 0 then ()
-    else match context.stack with
-    | Leaf -> assert false
-    | Node (node, child, pos, ctx) ->
-      let data = Buffer.contents pp_buffer in
-      let () = Buffer.clear pp_buffer in
-      let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in
-      context.offset <- context.offset + len
-  in
-
-  let open_xml_tag tag =
-    let () = push_pcdata () in
-    context.stack <- Node (tag, [], context.offset, context.stack)
-  in
-
-  let close_xml_tag tag =
-    let () = push_pcdata () in
-    match context.stack with
-    | 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;
-        startpos = pos;
-        endpos = context.offset;
-      } in
-      let xml = Element (node, annotation, List.rev child) in
-      match ctx with
-      | Leaf ->
-        (** Final node: we keep the result in a dummy context *)
-        context.stack <- Node ("", [xml], 0, Leaf)
-      | Node (node, child, pos, ctx) ->
-        context.stack <- Node (node, xml :: child, pos, ctx)
-  in
-
-  let open Format in
-
-  let ft = formatter_of_buffer pp_buffer in
-
-  let tag_functions = {
-    mark_open_tag = (fun tag -> let () = open_xml_tag tag in "");
-    mark_close_tag = (fun tag -> let () = close_xml_tag tag in "");
-    print_open_tag = ignore;
-    print_close_tag = ignore;
-  } in
-
-  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;
-  pp_set_max_indent ft m;
-
-  (** The whole output must be a valid document. To that
-      end, we nest the document inside <pp> tags. *)
-  pp_open_tag ft "pp";
-  Pp.(pp_with ~pp_tag ft ppcmds);
-  pp_close_tag ft ();
-
-  (** Get the resulting XML tree. *)
-  let () = pp_print_flush ft () in
-  let () = assert (Buffer.length pp_buffer = 0) in
-  match context.stack with
-  | Node ("", [xml], 0, Leaf) -> xml
-  | _ -> assert false
-
-
-let annotations_positions xml =
-  let rec node accu = function
-    | Element (_, { annotation = Some annotation; startpos; endpos }, cs) ->
-      children ((annotation, (startpos, endpos)) :: accu) cs
-    | Element (_, _, cs) ->
-      children accu cs
-    | _ ->
-      accu
-  and children accu cs =
-    List.fold_left node accu cs
-  in
-  node [] xml
-
-let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
-  let rec node = function
-    | Element (index, { annotation; startpos; endpos }, cs) ->
-      let attributes =
-        [ "startpos", string_of_int startpos;
-          "endpos", string_of_int endpos
-        ]
-        @ (match annotation with
-          | None -> []
-          | Some annotation -> attributes_of_annotation annotation
-        )
-      in
-      let tag =
-        match annotation with
-          | None -> index
-          | Some annotation -> tag_of_annotation annotation
-      in
-      Element (tag, attributes, List.map node cs)
-    | PCData s ->
-      PCData s
-  in
-  node 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 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)]
-  in
-  let xml = rich_pp annotate 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/lib/richpp.mli
deleted file mode 100644
index 287d265a8f..0000000000
--- a/lib/richpp.mli
+++ /dev/null
@@ -1,64 +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 offers semi-structured pretty-printing. *)
-
-(** Each annotation of the semi-structured document refers to the
-    substring it annotates. *)
-type 'annotation located = {
-  annotation : 'annotation option;
-  startpos   : int;
-  endpos     : int
-}
-
-(** [rich_pp get_annotations 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
-
-(** [annotations_positions ssdoc] returns a list associating each
-    annotations with its position in the string from which [ssdoc] is
-    built. *)
-val annotations_positions :
-  'annotation located Xml_datatype.gxml ->
-  ('annotation * (int * int)) list
-
-(** [xml_of_rich_pp ssdoc] returns an XML representation of the
-    semi-structured document [ssdoc]. *)
-val xml_of_rich_pp :
-  ('annotation -> string) ->
-  ('annotation -> (string * string) list) ->
-  'annotation located Xml_datatype.gxml ->
-  Xml_datatype.xml
-
-(** {5 Enriched text} *)
-
-type richpp
-(** Type of text with style annotations *)
-
-val richpp_of_pp : 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