[pp] Make feedback the only logging mechanism.

Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.

This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.

Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.

However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.

The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.

We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.

`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.

Thus, the new panorama is:

- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
  It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
  to coqtop.

_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.

_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.

A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.

The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.

10 files changed, 43 insertions, 613 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index a059640394..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.error_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
 
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 1e33173ee1..5a5f6afd39 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -15,7 +15,6 @@ Store
 Exninfo
 Backtrace
 IStream
-Pp_control
 Flags
 Control
 Loc
@@ -28,9 +27,8 @@ CStack
 Util
 Stateid
 Pp
-Ppstyle
-Richpp
 Feedback
+Ppstyle
 CUnix
 Envars
 Aux_file
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 852eec2f26..31677ecfc9 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,140 +45,6 @@ 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 =
-  pp_with ?pp_tag 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_str = tag Ppstyle.debug_tag   (str "Debug:")   ++ spc ()
-let info_str = mt ()
-let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc ()
-let  err_str = tag Ppstyle.error_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_format 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.to_format;
-  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 : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7
 
@@ -190,11 +56,6 @@ let add_feeder =
 
 let del_feeder fid = Hashtbl.remove feeders fid
 
-let debug_feeder = function
-  | { contents = Message (Debug, loc, pp) } ->
-       msg_debug ?loc (Pp.str (Richpp.raw_print pp))
-  | _ -> ()
-
 let feedback_id    = ref (Edit 0)
 let feedback_route = ref default_route
 
@@ -209,32 +70,16 @@ let feedback ?id ?route what =
   } in
   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))
+  feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, 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
+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
 
+let debug_feeder = function
+  | { contents = Message (Debug, loc, pp) } -> msg_debug ?loc pp
+  | _ -> ()
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 8eae315883..3fb7c0039e 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,32 +52,12 @@ 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
 
@@ -97,10 +76,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
@@ -128,7 +103,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 d763767dc2..5dba0356d8 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp_control
-
 (* The different kinds of blocks are:
    \begin{description}
    \item[hbox:] Horizontal block no line breaking;
@@ -178,10 +176,9 @@ let pp_with ?pp_tag ft =
     | 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)       -> (* Prevent evaluation of the stream! *)
-        cpp_open_box bty ;
-        if not (Format.over_max_boxes ()) then pp_cmd ss;
-        Format.pp_close_box ft ()
+    | 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
diff --git a/lib/pp.mli b/lib/pp.mli
index 5bf5391d3b..12747d3a1d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -8,6 +8,30 @@
 
 (** Coq document type. *)
 
+(** Pretty printing guidelines ******************************************)
+(*                                                                      *)
+(* std_ppcmds is the main pretty printing datatype in he Coq. Documents *)
+(* are composed laying out boxes, and users can add arbitrary metadata  *)
+(* that backends are free to interpret.                                 *)
+(*                                                                      *)
+(* The datatype is public to allow serialization or advanced uses,      *)
+(* regular users are _strongly_ encouraged to use the top-level         *)
+(* functions to manipulate the type.                                    *)
+(*                                                                      *)
+(* Box order and number is indeed an important factor. Users should try *)
+(* to create a proper amount of boxes. Also, the ++ operator provides   *)
+(* "efficient" concatenation, but directly using a list is 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")`            *)
+(*                                                                      *)
+(************************************************************************)
+
 (* XXX: Improve and add attributes *)
 type pp_tag = string list
 
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/richpp.ml b/lib/richpp.ml
deleted file mode 100644
index c0128dbc2d..0000000000
--- a/lib/richpp.ml
+++ /dev/null
@@ -1,200 +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 = Some (Ppstyle.repr t)    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 2e839e996b..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.pp_tag -> '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