[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.

17 files changed, 388 insertions, 92 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 9637b5b3f2..e2036beee3 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 option; (* last call + callback + log *)
+  mutable waiting_for : ccb option; (* last call + callback *)
 }
 
 (** Coqtop process status :
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 0f3629c8fc..7982ffc8b8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -162,13 +162,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 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
 
@@ -418,9 +421,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
@@ -466,7 +470,7 @@ 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
+          let msg = Pp.string_of_ppcmds msg      in
           log "ErrorMsg" id;
           remove_flag sentence `PROCESSING;
           add_flag sentence (`ERROR (loc, msg));
@@ -476,14 +480,15 @@ object(self)
             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 rmsg = Richpp.raw_print msg         in
-          log "WarningMsg" id;
+          let rmsg = Pp.string_of_ppcmds msg      in
+          log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id;
           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) ->
-        messages#push lvl msg
+          log ("Msg: " ^ Pp.string_of_ppcmds msg) id;
+          messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
@@ -629,10 +634,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));
@@ -646,7 +650,7 @@ object(self)
             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)) ->
@@ -654,7 +658,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)
@@ -673,7 +677,7 @@ 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 true) next
@@ -860,7 +864,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;
@@ -906,7 +910,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 3d56f9dd49..25858acced 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
 
@@ -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 ed1fa465d2..043ad6008b 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 72a14134bf..12170c4621 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,11 +9,11 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Serialize
-Richprinter
 Xml_lexer
 Xml_parser
 Xml_printer
+Serialize
+Richpp
 Xmlprotocol
 Ideutils
 Coq
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 0cb8d377f6..88b61042ed 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -32,9 +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 pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let pr_error s = pr_with_pid s
@@ -174,13 +171,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
@@ -340,13 +337,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 = 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 ()
@@ -446,7 +440,6 @@ 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_feeder xml_oc msg =
   let xml = Xmlprotocol.of_feedback msg in
   print_xml xml_oc xml
@@ -467,7 +460,6 @@ let loop () =
   (* 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 Feedback.feedback_logger;
   Feedback.add_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
@@ -478,7 +470,7 @@ 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 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);
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c3a2807967..498a911ee4 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -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 ~level (Pp.string_of_ppcmds message)
 
 
 (** {6 File operations} *)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index e32a4d9e38..1ae66e23e9 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -69,7 +69,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 123cac6c22..43446f3918 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
 
@@ -203,7 +202,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/richpp.ml b/ide/richpp.ml
new file mode 100644
index 0000000000..c0128dbc2d
--- /dev/null
+++ b/ide/richpp.ml
@@ -0,0 +1,200 @@
+(************************************************************************)
+(*  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/ide/richpp.mli b/ide/richpp.mli
new file mode 100644
index 0000000000..2e839e996b
--- /dev/null
+++ b/ide/richpp.mli
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  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
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index d33c0add4a..b83bd107ee 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -103,7 +103,7 @@ object(self)
       let process =
 	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
-            Ideutils.insert_xml result#buffer str;
+            Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp str);
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
 	    Coq.return ()
           | Interface.Good res ->
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 0330b8eff1..1cf389c75d 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -28,9 +28,9 @@ 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 push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
@@ -79,21 +79,14 @@ let message_view () : message_view =
       | 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
+      let mark = `MARK mark in
+      Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp msg);
+      buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
+      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
 
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 2d34533dee..a71d345a5f 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -18,9 +18,9 @@ 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 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 47c86045a5..72aa9051a0 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -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 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 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 g);
         proof#buffer#insert "\n"
       in
       let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
@@ -144,7 +144,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 goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter given_up_goals;
@@ -153,7 +153,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 goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter shelved_goals
@@ -166,7 +166,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 goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iteri iter bg
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 65f44fdd38..08f23d3d4e 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -97,6 +97,49 @@ 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 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_list 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
+  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_list 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_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
 | Fail (id,loc, msg) ->
@@ -104,7 +147,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 +163,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 +190,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 +387,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) =
@@ -701,10 +744,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 +803,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,12 +830,12 @@ 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 to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index ca911178f5..f6fae24d7c 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -66,5 +66,6 @@ val of_feedback : Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback
 val is_feedback : xml -> bool
 
-val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
+val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml
+(* val to_message : xml -> Feedback.message *)