Merge branch 'trunk' into pr379

23 files changed, 562 insertions, 342 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 6d44ca59e..3a1d87787 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -205,7 +205,7 @@ type handle = {
   proc : CoqTop.process;
   xml_oc : Xml_printer.t;
   mutable alive : bool;
-  mutable waiting_for : (ccb * logger) option; (* last call + callback + log *)
+  mutable waiting_for : ccb option; (* last call + callback *)
 }
 
 (** Coqtop process status :
@@ -290,18 +290,6 @@ let rec check_errors = function
 | `NVAL :: _ -> raise (TubeError "NVAL")
 | `OUT :: _ -> raise (TubeError "OUT")
 
-let handle_intermediate_message handle level content =
-  let logger  = match handle.waiting_for with
-    | Some (_, l) -> l
-    | None -> function
-        | Feedback.Error   -> fun s -> Minilib.log ~level:`ERROR   (xml_to_string s)
-        | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
-        | Feedback.Notice  -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
-        | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
-        | Feedback.Debug   -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
-  in
-  logger level content
-
 let handle_feedback feedback_processor xml =
   let feedback = Xmlprotocol.to_feedback xml in
   feedback_processor feedback
@@ -310,7 +298,7 @@ let handle_final_answer handle xml =
   let () = Minilib.log "Handling coqtop answer" in
   let ccb = match handle.waiting_for with
     | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml))
-    | Some (c, _) -> c in
+    | Some c -> c in
   let () = handle.waiting_for <- None in
   with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) }
 
@@ -332,18 +320,13 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     let l_end = Lexing.lexeme_end lex in
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
-    match Xmlprotocol.is_message xml with
-    | Some (lvl, _loc, msg) ->
-      handle_intermediate_message handle lvl msg;
+    if Xmlprotocol.is_feedback xml then begin
+      handle_feedback feedback_processor xml;
       loop ()
-    | None ->
-      if Xmlprotocol.is_feedback xml then begin
-        handle_feedback feedback_processor xml;
-        loop ()
-      end else
-        begin
-          ignore (handle_final_answer handle xml)
-        end
+    end else
+      begin
+        ignore (handle_final_answer handle xml)
+      end
   in
   try loop ()
   with Xml_parser.Error _ as e ->
@@ -383,7 +366,7 @@ let bind_self_as f =
 (** This launches a fresh handle from its command line arguments. *)
 let spawn_handle args respawner feedback_processor =
   let prog = coqtop_path () in
-  let args = Array.of_list ("-async-proofs" :: "on" :: "-ideslave" :: args) in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
   let env =
     match !Flags.ideslave_coqtop_flags with
     | None -> None
@@ -493,20 +476,20 @@ let init_coqtop coqtop task =
 
 type 'a query = 'a Interface.value task
 
-let eval_call ?(logger=default_logger) call handle k =
+let eval_call call handle k =
   (** Send messages to coqtop and prepare the decoding of the answer *)
   Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call);
   assert (handle.alive && handle.waiting_for = None);
-  handle.waiting_for <- Some (mk_ccb (call,k), logger);
+  handle.waiting_for <- Some (mk_ccb (call,k));
   Xml_printer.print handle.xml_oc (Xmlprotocol.of_call call);
   Minilib.log "End eval_call";
   Void
 
-let add ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.add x)
+let add x = eval_call (Xmlprotocol.add x)
 let edit_at i = eval_call (Xmlprotocol.edit_at i)
-let query ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.query x)
+let query x = eval_call (Xmlprotocol.query x)
 let mkcases s = eval_call (Xmlprotocol.mkcases s)
-let status ?logger force = eval_call ?logger (Xmlprotocol.status force)
+let status force = eval_call (Xmlprotocol.status force)
 let hints x = eval_call (Xmlprotocol.hints x)
 let search flags = eval_call (Xmlprotocol.search flags)
 let init x = eval_call (Xmlprotocol.init x)
@@ -566,18 +549,11 @@ struct
 
   let _ = reset ()
 
-  (** Integer option *)
-
-  let width = ["Printing"; "Width"]
-  let width_state = ref None
-  let set_printing_width w = width_state := Some w
-
   (** Transmitting options to coqtop *)
 
   let enforce h k =
     let mkopt o v acc = (o, Interface.BoolValue v) :: acc in
     let opts = Hashtbl.fold mkopt current_state [] in
-    let opts = (width, Interface.IntValue !width_state) :: opts in
     eval_call (Xmlprotocol.set_options opts) h
       (function
 	| Interface.Good () -> k ()
@@ -585,8 +561,8 @@ struct
 
 end
 
-let goals ?logger x h k =
-  PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k)
+let goals x h k =
+  PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.goals x) h k)
 
 let evars x h k =
   PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.evars x) h k)
diff --git a/ide/coq.mli b/ide/coq.mli
index 8a1fa3ed1..ab8c12a6f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -115,15 +115,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
 type 'a query = 'a Interface.value task
 (** A type abbreviation for coqtop specific answers *)
 
-val add        : ?logger:Ideutils.logger ->
-                 Interface.add_sty        -> Interface.add_rty query
+val add        : Interface.add_sty        -> Interface.add_rty query
 val edit_at    : Interface.edit_at_sty    -> Interface.edit_at_rty query
-val query      : ?logger:Ideutils.logger ->
-                 Interface.query_sty      -> Interface.query_rty query
-val status     : ?logger:Ideutils.logger ->
-                 Interface.status_sty     -> Interface.status_rty query
-val goals      : ?logger:Ideutils.logger ->
-                 Interface.goals_sty      -> Interface.goals_rty query
+val query      : Interface.query_sty      -> Interface.query_rty query
+val status     : Interface.status_sty     -> Interface.status_rty query
+val goals      : Interface.goals_sty      -> Interface.goals_rty query
 val evars      : Interface.evars_sty      -> Interface.evars_rty query
 val hints      : Interface.hints_sty      -> Interface.hints_rty query
 val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
@@ -143,7 +139,6 @@ sig
   val bool_items : bool_descr list
 
   val set : t -> bool -> unit
-  val set_printing_width : int -> unit
 
   (** [enforce] transmits to coq the current option values.
       It is also called by [goals] and [evars] above. *)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1563c7ffb..4a1d688f5 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -128,6 +128,9 @@ end = struct
 end
 open SentenceId
 
+let log_pp msg : unit task =
+  Coq.lift (fun () -> Minilib.log_pp msg)
+
 let log msg : unit task =
   Coq.lift (fun () -> Minilib.log msg)
 
@@ -162,13 +165,16 @@ let flags_to_color f =
   else if List.mem `INCOMPLETE f then `NAME "gray"
   else `NAME Preferences.processed_color#get
 
-let validate s =
-  let open Xml_datatype in
-  let rec validate = function
-  | PCData s -> Glib.Utf8.validate s
-  | Element (_, _, children) -> List.for_all validate children
-  in
-  validate (Richpp.repr s)
+(* Move to utils? *)
+let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with
+  | Pp.Ppcmd_empty
+  | Pp.Ppcmd_print_break _
+  | Pp.Ppcmd_force_newline  -> true
+  | Pp.Ppcmd_glue l    -> List.for_all validate l
+  | Pp.Ppcmd_string s  -> Glib.Utf8.validate s
+  | Pp.Ppcmd_box (_,s)
+  | Pp.Ppcmd_tag (_,s) -> validate s
+  | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s
 
 module Doc = Document
 
@@ -305,7 +311,7 @@ object(self)
 
   method private print_stack =
     Minilib.log "document:";
-    Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer)))
+    Minilib.log_pp (Doc.print document (dbg_to_string buffer))
 
   method private enter_focus start stop =
     let at id id' _ = Stateid.equal id' id in
@@ -337,7 +343,6 @@ object(self)
     buffer#get_iter_at_mark `INSERT
 
   method private show_goals_aux ?(move_insert=false) () =
-    Coq.PrintOpt.set_printing_width proof#width;
     if move_insert then begin
       let dest = self#get_start_of_input in
       if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin
@@ -345,7 +350,7 @@ object(self)
         script#recenter_insert
       end
     end;
-    Coq.bind (Coq.goals ~logger:messages#push ()) (function
+    Coq.bind (Coq.goals ()) (function
     | Fail x -> self#handle_failure_aux ~move_insert x
     | Good goals ->
       Coq.bind (Coq.evars ()) (function
@@ -368,7 +373,7 @@ object(self)
       else messages#add s;
     in
     let query =
-      Coq.query ~logger:messages#push (phrase,Stateid.dummy) in
+      Coq.query (phrase,Stateid.dummy) in
     let next = function
     | Fail (_, _, err) -> display_error err; Coq.return ()
     | Good msg ->
@@ -377,8 +382,7 @@ object(self)
     Coq.bind (Coq.seq action query) next
 
   method private mark_as_needed sentence =
-    Minilib.log("Marking " ^
-      Pp.string_of_ppcmds (dbg_to_string buffer false None sentence));
+    Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
     let to_process = Tags.Script.to_process in
@@ -418,9 +422,10 @@ object(self)
     | _ -> false
 
   method private enqueue_feedback msg =
+    (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
     let id = msg.id in
     if self#is_dummy_id id then () else Queue.add msg feedbacks
-    
+
   method private process_feedback () =
     let rec eat_feedback n =
       if n = 0 then true else
@@ -434,9 +439,11 @@ object(self)
           | _ -> None in
         try Some (Doc.find_map document finder)
         with Not_found -> None in
-      let log s state_id =
-        Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string
-          (Option.default Stateid.dummy state_id)) in
+      let log_pp s state_id =
+        Minilib.log_pp Pp.(seq
+                [str "Feedback "; s; str " on ";
+                 str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in
+      let log s state_id = log_pp (Pp.str s) state_id in
       begin match msg.contents, sentence with
       | AddedAxiom, Some (id,sentence) ->
           log "AddedAxiom" id;
@@ -466,22 +473,24 @@ object(self)
             (Printf.sprintf "%s %s %s" filepath ident ty)
       | Message(Error, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let msg = Richpp.raw_print msg         in
-          log "ErrorMsg" id;
+          log_pp Pp.(str "ErrorMsg" ++ msg) id;
           remove_flag sentence `PROCESSING;
-          add_flag sentence (`ERROR (loc, msg));
+          let rmsg = Pp.string_of_ppcmds msg     in
+          add_flag sentence (`ERROR (loc, rmsg));
           self#mark_as_needed sentence;
-          self#attach_tooltip sentence loc msg;
+          self#attach_tooltip sentence loc rmsg;
           if not (Loc.is_ghost loc) then
             self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
       | Message(Warning, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let msg = Richpp.raw_print msg         in
-          log "WarningMsg" id;
-          add_flag sentence (`WARNING (loc, msg));
-          self#attach_tooltip sentence loc msg;
-          self#position_warning_tag_at_sentence sentence loc
-      | Message((Info|Notice|Debug as lvl), _, msg), _ ->
+          log_pp Pp.(str "WarningMsg" ++ msg) id;
+          let rmsg = Pp.string_of_ppcmds msg     in
+          add_flag sentence (`WARNING (loc, rmsg));
+          self#attach_tooltip sentence loc rmsg;
+          self#position_warning_tag_at_sentence sentence loc;
+          messages#push Warning msg
+      | Message(lvl, loc, msg), Some (id,sentence) ->
+          log_pp Pp.(str "Msg" ++ msg) id;
           messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
@@ -628,10 +637,9 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-
-            logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
+            logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted");
             self#discard_command_queue queue;
-            conclude [] 
+            conclude []
         | `Skip(start,stop), (_,s) :: topstack ->
             assert(start#equal (buffer#get_iter_at_mark s.start));
             assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -641,11 +649,11 @@ object(self)
             add_flag sentence `PROCESSING;
             Doc.push document sentence;
             let _, _, phrase = self#get_sentence sentence in
-            let coq_query = Coq.add ~logger ((phrase,edit_id),(tip,verbose)) in
+            let coq_query = Coq.add ((phrase,edit_id),(tip,verbose)) in
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Feedback.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Pp.str msg);
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -653,7 +661,7 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Feedback.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Pp.str msg);
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
@@ -672,10 +680,10 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
+         messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
-   Coq.bind (Coq.status ~logger:messages#push true) next
+   Coq.bind (Coq.status true) next
 
   method stop_worker n =
     Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ())
@@ -859,7 +867,7 @@ object(self)
       let next = function
       | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
-        messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
+        messages#add (Pp.str ("Unsuccessfully tried: "^phrase));
         more
       | Good msg ->
         messages#add_string msg;
@@ -905,7 +913,7 @@ object(self)
     let get_initial_state =
       let next = function
       | Fail (_, _, message) ->
-        let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+        let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds message) in
         let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
         ignore (popup#run ()); exit 1
       | Good id -> initial_state <- id; Coq.return () in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 450bfcdfb..25858acce 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -318,7 +318,7 @@ let export kind sn =
         local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
         (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
       in
-      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+      sn.messages#set (Pp.str ("Running: "^cmd));
       let finally st = flash_info (cmd ^ pr_exit_status st)
       in
       run_command (fun msg -> sn.messages#add_string msg) finally cmd
@@ -431,7 +431,7 @@ let compile sn =
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-      sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+      sn.messages#set (Pp.str ("Running: "^cmd));
       let display s =
         sn.messages#add_string s;
         Buffer.add_string buf s
@@ -441,8 +441,8 @@ let compile sn =
           flash_info (f ^ " successfully compiled")
         else begin
           flash_info (f ^ " failed to compile");
-          sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
-          sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf));
+          sn.messages#set (Pp.str "Compilation output:\n");
+          sn.messages#add (Pp.str (Buffer.contents buf));
         end
       in
       run_command display finally cmd
@@ -464,7 +464,7 @@ let make sn =
     |Some f ->
       File.saveall ();
       let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
-      sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
+      sn.messages#set (Pp.str "Compilation output:\n");
       Buffer.reset last_make_buf;
       last_make := "";
       last_make_index := 0;
@@ -508,11 +508,11 @@ let next_error sn =
     let stopi = b#get_iter_at_byte ~line:(line-1) stop in
     b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
     b#place_cursor ~where:starti;
-    sn.messages#set (Richpp.richpp_of_string error_msg);
+    sn.messages#set (Pp.str error_msg);
     sn.script#misc#grab_focus ()
   with Not_found ->
     last_make_index := 0;
-    sn.messages#set (Richpp.richpp_of_string "No more errors.\n")
+    sn.messages#set (Pp.str "No more errors.\n")
 
 let next_error = cb_on_current_term next_error
 
@@ -536,7 +536,7 @@ let update_status sn =
     display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name);
     Coq.return ()
   in
-  Coq.bind (Coq.status ~logger:sn.messages#push false) next
+  Coq.bind (Coq.status false) next
 
 let find_next_occurrence ~backward sn =
   (** go to the next occurrence of the current word, forward or backward *)
@@ -789,7 +789,7 @@ let coqtop_arguments sn =
         let args = String.concat " " args in
         let msg = Printf.sprintf "Invalid arguments: %s" args in
         let () = sn.messages#clear in
-        sn.messages#push Feedback.Error (Richpp.richpp_of_string msg)
+        sn.messages#push Feedback.Error (Pp.str msg)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ok_cb in
@@ -887,8 +887,8 @@ let alpha_items menu_name item_name l =
     | [] -> ()
     | [s] -> mk_item s
     | s::_ as ll ->
-      let name = item_name^" "^(String.make 1 s.[0]) in
-      let label = "_@..." in label.[1] <- s.[0];
+      let name = Printf.sprintf "%s %c" item_name s.[0] in
+      let label = Printf.sprintf "_%c..." s.[0] in
       item name ~label menu_name;
       List.iter mk_item ll
   in
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index ed1fa465d..043ad6008 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -2,7 +2,7 @@ Xml_lexer
 Xml_parser
 Xml_printer
 Serialize
-Richprinter
+Richpp
 Xmlprotocol
 Texmacspp
 Document
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 72a14134b..78b4c01e8 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,11 +9,12 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Serialize
-Richprinter
 Xml_lexer
 Xml_parser
 Xml_printer
+Serialize
+Richpp
+Topfmt
 Xmlprotocol
 Ideutils
 Coq
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 4967ddb75..0dfa03cca 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -32,24 +32,6 @@ let init_signal_handler () =
   let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
   Sys.set_signal Sys.sigint (Sys.Signal_handle f)
 
-
-(** Redirection of standard output to a printable buffer *)
-
-let init_stdout, read_stdout =
-  let out_buff = Buffer.create 100 in
-  let out_ft = Format.formatter_of_buffer out_buff in
-  let deep_out_ft = Format.formatter_of_buffer out_buff in
-  let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
-  (fun () ->
-     flush_all ();
-     Pp_control.std_ft := out_ft;
-     Pp_control.err_ft := out_ft;
-     Pp_control.deep_ft := deep_out_ft;
-  ),
-  (fun () -> Format.pp_print_flush out_ft ();
-             let r = Buffer.contents out_buff in
-             Buffer.clear out_buff; r)
-
 let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let pr_error s = pr_with_pid s
@@ -97,42 +79,58 @@ let is_undo cmd = match cmd with
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false
 
-(** Check whether a command is forbidden by CoqIDE *)
+(** Check whether a command is forbidden in the IDE *)
 
-let coqide_cmd_checks (loc,ast) =
+let ide_cmd_checks (loc,ast) =
   let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
   if is_debug ast then
-    user_error "Debug mode not available within CoqIDE";
+    user_error "Debug mode not available in the IDE";
   if is_known_option ast then
-    Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead");
+    Feedback.msg_warning (strbrk "Set this option from the IDE menu instead");
   if Vernac.is_navigation_vernac ast || is_undo ast then
-    Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead");
+    Feedback.msg_warning (strbrk "Use IDE navigation instead");
   if is_query ast then
     Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
 let add ((s,eid),(sid,verbose)) =
-  let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in
+  let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
-  newid, (rc, read_stdout ())
+  (* TODO: the "" parameter is a leftover of the times the protocol
+   * used to include stderr/stdout output.
+   *
+   * Currently, we force all the output meant for the to go via the
+   * feedback mechanism, and we don't manipulate stderr/stdout, which
+   * are left to the client's discrection. The parameter is still there
+   * as not to break the core protocol for this minor change, but it should
+   * be removed in the next version of the protocol.
+   *)
+  newid, (rc, "")
 
 let edit_at id =
   match Stm.edit_at id with
   | `NewTip -> CSig.Inl ()
   | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip))
 
-let query (s,id) = Stm.query ~at:id s; read_stdout ()
+(* TODO: the "" parameter is a leftover of the times the protocol
+ * used to include stderr/stdout output.
+ *
+ * Currently, we force all the output meant for the to go via the
+ * feedback mechanism, and we don't manipulate stderr/stdout, which
+ * are left to the client's discrection. The parameter is still there
+ * as not to break the core protocol for this minor change, but it should
+ * be removed in the next version of the protocol.
+ *)
+let query (s,id) = Stm.query ~at:id s; ""
 
 let annotate phrase =
   let (loc, ast) =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
     Vernac.parse_sentence (pa,None)
   in
-  let (_, xml) =
-    Richprinter.richpp_vernac ast
-  in
-  xml
+  (* XXX: Width should be a parameter of annotate... *)
+  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
 
 (** Goal display *)
 
@@ -192,13 +190,13 @@ let process_goal sigma g =
   let id = Goal.uid g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
+    pr_goal_concl_style_env env sigma norm_constr
   in
   let process_hyp d (env,l) =
     let d = CompactedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_evar sigma (EConstr.of_constr c))) d in
     let d' = CompactedDecl.to_named_context d in
       (List.fold_right Environ.push_named d' env,
-       (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in
+       (pr_compacted_decl env sigma d) :: l) in
   let (_env, hyps) =
     Context.Compacted.fold process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
@@ -214,8 +212,6 @@ let export_pre_goals pgs =
 
 let goals () =
   Stm.finish ();
-  let s = read_stdout () in
-  if not (String.is_empty s) then Feedback.msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
     Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
@@ -224,8 +220,6 @@ let goals () =
 let evars () =
   try
     Stm.finish ();
-    let s = read_stdout () in
-    if not (String.is_empty s) then Feedback.msg_info (str s);
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
     let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in
@@ -257,8 +251,6 @@ let status force =
       and display the other parts (opened sections and modules) *)
   Stm.finish ();
   if force then Stm.join ();
-  let s = read_stdout () in
-  if not (String.is_empty s) then Feedback.msg_info (str s);
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
@@ -281,7 +273,7 @@ let status force =
 let export_coq_object t = {
   Interface.coq_object_prefix = t.Search.coq_object_prefix;
   Interface.coq_object_qualid = t.Search.coq_object_qualid;
-  Interface.coq_object_object = t.Search.coq_object_object
+  Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
 }
 
 let pattern_of_string ?env s =
@@ -364,14 +356,10 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg () =
-    let msg = read_stdout () in
-    let msg = str msg ++ fnl () ++ CErrors.print ~info e in
-    Richpp.richpp_of_pp msg
-  in
+  let mk_msg () = CErrors.print ~info e in
   match e with
-  | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
-  | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
+  | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
+  | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
       | Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -409,7 +397,16 @@ let interp ((_raw, verbose), s) =
       | Some ast -> ast)
     () in
   Stm.interp verbose (vernac_parse s);
-  Stm.get_current_state (), CSig.Inl (read_stdout ())
+  (* TODO: the "" parameter is a leftover of the times the protocol
+   * used to include stderr/stdout output.
+   *
+   * Currently, we force all the output meant for the to go via the
+   * feedback mechanism, and we don't manipulate stderr/stdout, which
+   * are left to the client's discrection. The parameter is still there
+   * as not to break the core protocol for this minor change, but it should
+   * be removed in the next version of the protocol.
+   *)
+  Stm.get_current_state (), CSig.Inl ""
 
 (** When receiving the Quit call, we don't directly do an [exit 0],
     but rather set this reference, in order to send a final answer
@@ -428,14 +425,12 @@ let print_ast id =
 
 (** Grouping all call handlers together + error handling *)
 
-let eval_call xml_oc log c =
+let eval_call c =
   let interruptible f x =
     catch_break := true;
     Control.check_for_interrupt ();
     let r = f x in
     catch_break := false;
-    let out = read_stdout () in
-    if not (String.is_empty out) then log (str out);
     r
   in
   let handler = {
@@ -473,16 +468,8 @@ let print_xml =
     try Xml_printer.print oc xml; Mutex.unlock m
     with e -> let e = CErrors.push e in Mutex.unlock m; iraise e
 
-
-let slave_logger xml_oc ?loc level message =
-  (* convert the message into XML *)
-  let msg = hov 0 message in
-  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))         in
-  let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in
-  print_xml xml_oc xml
-
-let slave_feeder xml_oc msg =
-  let xml = Xmlprotocol.of_feedback msg in
+let slave_feeder fmt xml_oc msg =
+  let xml = Xmlprotocol.(of_feedback fmt msg) in
   print_xml xml_oc xml
 
 (** The main loop *)
@@ -491,17 +478,22 @@ let slave_feeder xml_oc msg =
     messages by [handle_exn] above. Otherwise, we die badly, without
     trying to answer malformed requests. *)
 
+let msg_format = ref (fun () ->
+    let margin = Option.default 72 (Topfmt.get_margin ()) in
+    Xmlprotocol.Richpp margin
+)
+
 let loop () =
   init_signal_handler ();
   catch_break := false;
-  let in_ch, out_ch = Spawned.get_channels () in
-  let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in
-  let in_lb = Lexing.from_function (fun s len ->
-    CThread.thread_friendly_read in_ch s ~off:0 ~len) in
-  let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
+  let in_ch, out_ch = Spawned.get_channels ()                        in
+  let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in
+  let in_lb         = Lexing.from_function (fun s len ->
+                      CThread.thread_friendly_read in_ch s ~off:0 ~len) in
+  (* SEXP parser make *)
+  let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
-  Feedback.set_logger (slave_logger xml_oc);
-  Feedback.add_feeder (slave_feeder xml_oc);
+  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -511,10 +503,10 @@ let loop () =
 (*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
       let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
-      let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) q in
+      let r  = eval_call q in
       let () = pr_debug_answer q r in
 (*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
-      print_xml xml_oc (Xmlprotocol.of_answer q r);
+      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);
       flush out_ch
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->
@@ -536,16 +528,19 @@ let loop () =
 let rec parse = function
   | "--help-XML-protocol" :: rest ->
         Xmlprotocol.document Xml_printer.to_string_fmt; exit 0
+  | "--xml_format=Ppcmds" :: rest ->
+        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest
   | x :: rest -> x :: parse rest
   | [] -> []
 
 let () = Coqtop.toploop_init := (fun args ->
         let args = parse args in
         Flags.make_silent true;
-        init_stdout ();
         CoqworkmgrApi.(init Flags.High);
         args)
 
 let () = Coqtop.toploop_run := loop
 
-let () = Usage.add_to_usage "coqidetop" "  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
+let () = Usage.add_to_usage "coqidetop"
+"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format
+  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 06a132732..da867e689 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -43,7 +43,7 @@ let xml_to_string xml =
   | Element (_, _, children) ->
     List.iter iter children
   in
-  let () = iter (Richpp.repr xml) in
+  let () = iter xml in
   Buffer.contents buf
 
 let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
@@ -75,7 +75,7 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
     let tags = try tag t :: tags with Not_found -> tags in
     List.iter (fun xml -> insert tags xml) children
   in
-  let () = try insert tags (Richpp.repr msg) with _ -> () in
+  let () = try insert tags msg with _ -> () in
   buf#delete_mark rmark
 
 let set_location = ref  (function s -> failwith "not ready")
@@ -294,18 +294,20 @@ let coqtop_path () =
       match cmd_coqtop#get with
 	| Some s -> s
 	| None ->
-	  let prog = String.copy Sys.executable_name in
 	  try
-	    let pos = String.length prog - 6 in
-	    let i = Str.search_backward (Str.regexp_string "coqide") prog pos
+            let old_prog = Sys.executable_name in
+            let pos = String.length old_prog - 6 in
+            let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
             in
-	    String.blit "coqtop" 0 prog i 6;
-	    if Sys.file_exists prog then prog
+            let new_prog = Bytes.of_string old_prog in
+            Bytes.blit_string "coqtop" 0 new_prog i 6;
+            let new_prog = Bytes.to_string new_prog in
+            if Sys.file_exists new_prog then new_prog
 	    else
 	      let in_macos_bundle =
 		Filename.concat
-		  (Filename.dirname prog)
-		  (Filename.concat "../Resources/bin" (Filename.basename prog))
+		  (Filename.dirname new_prog)
+		  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
 	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
 		 else "coqtop"
 	  with Not_found -> "coqtop"
@@ -325,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
@@ -335,7 +337,7 @@ let default_logger level message =
   | Feedback.Warning -> `WARNING
   | Feedback.Error -> `ERROR
   in
-  Minilib.log ~level (xml_to_string message)
+  Minilib.log_pp ~level message
 
 
 (** {6 File operations} *)
@@ -357,7 +359,7 @@ let stat f =
 
 let maxread = 4096
 
-let read_string = String.create maxread
+let read_string = Bytes.create maxread
 let read_buffer = Buffer.create maxread
 
 (** Read the content of file [f] and add it to buffer [b].
@@ -368,7 +370,7 @@ let read_file name buf =
   let len = ref 0 in
   try
     while len := input ic read_string 0 maxread; !len > 0 do
-      Buffer.add_substring buf read_string 0 !len
+      Buffer.add_subbytes buf read_string 0 !len
     done;
     close_in ic
   with e -> close_in ic; raise e
@@ -381,8 +383,9 @@ let read_file name buf =
 let io_read_all chan =
   Buffer.clear read_buffer;
   let read_once () =
-    let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in
-    Buffer.add_substring read_buffer read_string 0 len
+    (* XXX: Glib.Io must be converted to bytes / -safe-string upstream *)
+    let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in
+    Buffer.add_subbytes read_buffer read_string 0 len
   in
   begin
     try while true do read_once () done
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index e32a4d9e3..4b4ba72b0 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,8 +52,6 @@ val pop_info : unit -> unit
 val clear_info : unit -> unit
 val flash_info : ?delay:int -> string -> unit
 
-val xml_to_string : Richpp.richpp -> string
-
 val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
@@ -69,7 +67,7 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Feedback.level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Pp.std_ppcmds -> unit
 
 val default_logger : logger
 (** Default logger. It logs messages that the casual user should not see. *)
diff --git a/ide/interface.mli b/ide/interface.mli
index 123cac6c2..9ed606258 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -12,15 +12,14 @@
 
 type raw = bool
 type verbose = bool
-type richpp = Richpp.richpp
 
 (** The type of coqtop goals *)
 type goal = {
   goal_id : string;
   (** Unique goal identifier *)
-  goal_hyp : richpp list;
+  goal_hyp : Pp.std_ppcmds list;
   (** List of hypotheses *)
-  goal_ccl : richpp;
+  goal_ccl : Pp.std_ppcmds;
   (** Goal conclusion *)
 }
 
@@ -119,7 +118,7 @@ type edit_id = Feedback.edit_id
    should probably retract to that point *)
 type 'a value =
   | Good of 'a
-  | Fail of (state_id * location * richpp)
+  | Fail of (state_id * location * Pp.std_ppcmds)
 
 type ('a, 'b) union = ('a, 'b) Util.union
 
@@ -128,9 +127,13 @@ type ('a, 'b) union = ('a, 'b) Util.union
 (**  [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid]
      on top of the current edit position (that is asserted to be [sid])
      verbosely if [v] is true.  The response [(id,(rc,s)] is the new state
-     [id] assigned to the phrase, some output [s].  [rc] is [Inl] if the new
+     [id] assigned to the phrase. [rc] is [Inl] if the new
      state id is the tip of the edit point, or [Inr tip] if the new phrase
-     closes a focus and [tip] is the new edit tip *)
+     closes a focus and [tip] is the new edit tip
+
+     [s] used to contain Coq's console output and has been deprecated
+     in favor of sending feedback, it will be removed in a future
+     version of the protocol.  *)
 type add_sty = (string * edit_id) * (state_id * verbose)
 type add_rty = state_id * ((unit, state_id) union * string)
 
@@ -143,8 +146,12 @@ type add_rty = state_id * ((unit, state_id) union * string)
 type edit_at_sty = state_id
 type edit_at_rty = (unit, state_id * (state_id * state_id)) union
 
-(** [query s id] executes [s] at state [id] and does not record any state
-    change but for the printings that are sent in response *)
+(** [query s id] executes [s] at state [id].
+
+    query used to reply with the contents of Coq's console output, and
+    has been deprecated in favor of sending the query answers as
+    feedback. It will be removed in a future version of the protocol.
+*)
 type query_sty = string * state_id
 type query_rty = string
 
@@ -203,7 +210,7 @@ type about_sty = unit
 type about_rty = coq_info
 
 type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * richpp
+type handle_exn_rty = state_id * location * Pp.std_ppcmds
 
 (* Retrocompatibility stuff *)
 type interp_sty = (raw * verbose) * string
diff --git a/ide/minilib.ml b/ide/minilib.ml
index d11e8c56b..2c24e46f8 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -30,7 +30,7 @@ let debug = ref false
    print in the response buffer.
 *)
 
-let log ?(level = `DEBUG) msg =
+let log_pp ?(level = `DEBUG) msg =
   let prefix = match level with
   | `DEBUG -> "DEBUG"
   | `INFO -> "INFO"
@@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg =
   | `FATAL -> "FATAL"
   in
   if !debug then begin
-    try Printf.eprintf "[%s] %s\n%!" prefix msg
+    try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg
     with _ -> ()
   end
 
+let log ?level str = log_pp ?level (Pp.str str)
+
 let coqify d = Filename.concat d "coq"
 
 let coqide_config_home () =
diff --git a/ide/minilib.mli b/ide/minilib.mli
index b7672c900..4517a2374 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -22,7 +22,8 @@ type level = [
 (** debug printing *)
 val debug : bool ref
 
-val log : ?level:level -> string -> unit
+val log_pp : ?level:level -> Pp.std_ppcmds -> unit
+val log    : ?level:level -> string        -> unit
 
 val coqide_config_home : unit -> string
 val coqide_config_dirs : unit -> string list
diff --git a/ide/richpp.ml b/ide/richpp.ml
new file mode 100644
index 000000000..522a3e0b3
--- /dev/null
+++ b/ide/richpp.ml
@@ -0,0 +1,169 @@
+(************************************************************************)
+(*  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 *)
+}
+
+(** 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 width ppcmds =
+
+  let context = {
+    stack = Leaf;
+    offset = 0;
+  } 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 = {
+        annotation = Some tag;
+        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;
+
+  (* Setting the formatter *)
+  pp_set_margin ft width;
+  let m = max (64 * width / 100) (width-30) in
+  pp_set_max_indent ft m;
+  pp_set_max_boxes ft 50 ;
+  pp_set_ellipsis_text ft "...";
+
+  (** The whole output must be a valid document. To that
+      end, we nest the document inside <pp> tags. *)
+  pp_open_box ft 0;
+  pp_open_tag ft "pp";
+  Pp.(pp_with ft ppcmds);
+  pp_close_tag ft ();
+  pp_close_box 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 richpp_of_pp width pp =
+  let rec drop = function
+  | PCData s -> [PCData s]
+  | Element (_, annotation, cs) ->
+    let cs = List.concat (List.map drop cs) in
+    match annotation.annotation with
+    | None -> cs
+    | Some s -> [Element (s, [], cs)]
+  in
+  let xml = rich_pp width pp in
+  Element ("_", [], drop xml)
diff --git a/ide/richpp.mli b/ide/richpp.mli
new file mode 100644
index 000000000..ea4b189ba
--- /dev/null
+++ b/ide/richpp.mli
@@ -0,0 +1,51 @@
+(************************************************************************)
+(*  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
+}
+
+(* XXX: The width parameter should be moved to a `formatter_property`
+   record shared with Topfmt *)
+
+(** [rich_pp width ppcmds] returns the interpretation
+    of [ppcmds] as a semi-structured document
+    that represents (located) annotations of this string.
+    The [get_annotations] function is used to convert tags into the desired
+    annotation. [width] sets the printing witdh of the formatter. *)
+val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml
+
+(** [annotations_positions ssdoc] returns a list associating each
+    annotations with its position in the string from which [ssdoc] is
+    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 = Xml_datatype.xml
+
+(** Type of text with style annotations *)
+
+val richpp_of_pp : int -> Pp.std_ppcmds -> richpp
+(** Extract style information from formatted text *)
diff --git a/ide/richprinter.ml b/ide/richprinter.ml
deleted file mode 100644
index 995cef1ac..000000000
--- a/ide/richprinter.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-open Richpp
-
-module RichppConstr = Ppconstr.Richpp
-module RichppVernac = Ppvernac.Richpp
-
-type rich_pp =
-    Ppannotation.t Richpp.located Xml_datatype.gxml
-    * Xml_datatype.xml
-
-let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
-
-let make_richpp pr ast =
-  let rich_pp =
-    rich_pp get_annotations (pr ast)
-  in
-  let xml = Ppannotation.(
-    xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
-  )
-  in
-  (rich_pp, xml)
-
-let richpp_vernac = make_richpp RichppVernac.pr_vernac
-let richpp_constr = make_richpp RichppConstr.pr_constr_expr
diff --git a/ide/richprinter.mli b/ide/richprinter.mli
deleted file mode 100644
index c9e84e3eb..000000000
--- a/ide/richprinter.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This module provides an entry point to "rich" pretty-printers that
-    produce pretty-printing as done by {!Printer} but with additional
-    annotations represented as a semi-structured document.
-
-    To understand what are these annotations and how they are represented
-    as standard XML attributes, please refer to {!Ppannotation}.
-
-    In addition to these annotations, each node of the semi-structured
-    document contains a [startpos] and an [endpos] attribute that
-    relate this node to the raw pretty-printing.
-    Please refer to {!Richpp} for more details. *)
-
-(** A rich pretty-print is composed of: *)
-type rich_pp =
-
-    (** - a generalized semi-structured document whose attributes are
-        annotations ; *)
-    Ppannotation.t Richpp.located Xml_datatype.gxml
-
-    (** - an XML document, representing annotations as usual textual
-        XML attributes. *)
-    * Xml_datatype.xml
-
-(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *)
-val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
-
-(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
-val richpp_constr : Constrexpr.constr_expr -> rich_pp
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 946aaf010..47dad8f19 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,18 +100,15 @@ object(self)
         if Str.string_match (Str.regexp "\\. *$") com 0 then com
         else com ^ " " ^ arg ^" . "
       in
-      let log level message =
-        Ideutils.insert_xml result#buffer message;
-        result#buffer#insert "\n";
-      in
       let process =
-	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
+	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
-            Ideutils.insert_xml result#buffer str;
+            let width = Ideutils.textview_width result in
+            Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str);
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
 	    Coq.return ()
           | Interface.Good res ->
-            result#buffer#insert res; 
+            result#buffer#insert res;
             notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
 	    Coq.return ())
       in
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 0330b8eff..3d0cd46cd 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -28,9 +28,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : Richpp.richpp -> unit
+    method add : Pp.std_ppcmds -> unit
     method add_string : string -> unit
-    method set : Richpp.richpp -> unit
+    method set : Pp.std_ppcmds -> unit
+    method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
@@ -57,46 +58,71 @@ let message_view () : message_view =
   let () = view#set_left_margin 2 in
   view#misc#show ();
   let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed cb in
-  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let _ = background_color#connect#changed ~callback:cb in
+  let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
-  object (self)
+
+  (* Inserts at point, advances the mark *)
+  let insert_msg (level, msg) =
+    let tags = match level with
+      | Feedback.Error   -> [Tags.Message.error]
+      | Feedback.Warning -> [Tags.Message.warning]
+      | _ -> []
+    in
+    let mark = `MARK mark in
+    let width = Ideutils.textview_width view in
+    Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp width msg);
+    buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"
+  in
+
+  let mv = object (self)
     inherit GObj.widget box#as_widget
 
+    (* List of displayed messages *)
+    val mutable last_width = -1
+    val mutable msgs = []
+
     val push = new GUtil.signal ()
 
     method connect =
       new message_view_signals_impl box#as_widget push
 
+    method refresh force =
+      (* We need to block updates here due to the following race:
+         insertion of messages may create a vertical scrollbar, this
+         will trigger a width change, calling refresh again and
+         going into an infinite loop. *)
+      let width = Ideutils.textview_width view  in
+      (* Could still this method race if the scrollbar changes the
+         textview_width ?? *)
+      let needed = force || last_width <> width in
+      if needed then begin
+        last_width <- width;
+        buffer#set_text "";
+        buffer#move_mark (`MARK mark) ~where:buffer#start_iter;
+        List.(iter insert_msg (rev msgs))
+      end
+
     method clear =
-      buffer#set_text "";
-      buffer#move_mark (`MARK mark) ~where:buffer#start_iter
+      msgs <- []; self#refresh true
 
     method push level msg =
-      let tags = match level with
-      | Feedback.Error -> [Tags.Message.error]
-      | Feedback.Warning -> [Tags.Message.warning]
-      | _ -> []
-      in
-      let rec non_empty = function
-      | Xml_datatype.PCData "" -> false
-      | Xml_datatype.PCData _ -> true
-      | Xml_datatype.Element (_, _, children) -> List.exists non_empty children
-      in
-      if non_empty (Richpp.repr msg) then begin
-        let mark = `MARK mark in
-        Ideutils.insert_xml ~mark buffer ~tags msg;
-        buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
-        push#call (level, msg)
-      end
+      msgs <- (level, msg) :: msgs;
+      insert_msg (level, msg);
+      push#call (level, msg)
 
     method add msg = self#push Feedback.Notice msg
 
-    method add_string s = self#add (Richpp.richpp_of_string s)
+    method add_string s = self#add (Pp.str s)
 
     method set msg = self#clear; self#add msg
 
     method buffer = text_buffer
 
   end
+  in
+  (* Is there a better way to connect the signal ? *)
+  let w_cb (_ : Gtk.rectangle) = mv#refresh false in
+  ignore (view#misc#connect#size_allocate ~callback:w_cb);
+  mv
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 2d34533de..d065fcbc8 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -18,9 +18,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : Richpp.richpp -> unit
+    method add : Pp.std_ppcmds -> unit
     method add_string : string -> unit
-    method set : Richpp.richpp -> unit
+    method set : Pp.std_ppcmds -> unit
+    method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 47c86045a..b5405570c 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -18,7 +18,6 @@ class type proof_view =
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
-    method width : int
   end
 
 (* tag is the tag to be hooked, item is the item covered by this tag, make_menu
@@ -74,6 +73,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
       | None -> [], []
       | Some (hl, h) -> (hl, h)
       in
+      let width = Ideutils.textview_width proof in
       let rec insert_hyp hints hs = match hs with
       | [] -> ()
       | hyp :: hs ->
@@ -84,7 +84,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           let () = hook_tag_cb tag hint sel_cb on_hover in
           [tag], hints
         in
-        let () = insert_xml ~tags proof#buffer hyp in
+        let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp width hyp) in
         proof#buffer#insert "\n";
         insert_hyp rem_hints hs
       in
@@ -98,13 +98,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        insert_xml proof#buffer cur_goal;
+        insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal);
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
         proof#buffer#insert (goal_str i goals_cnt);
-        insert_xml proof#buffer g;
+        insert_xml proof#buffer (Richpp.richpp_of_pp width g);
         proof#buffer#insert "\n"
       in
       let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
@@ -122,6 +122,7 @@ let rec flatten = function
 
 let display mode (view : #GText.view_skel) goals hints evars =
   let () = view#buffer#set_text "" in
+  let width = Ideutils.textview_width view in
   match goals with
   | None -> ()
     (* No proof in progress *)
@@ -144,7 +145,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* The proof is finished, with the exception of given up goals. *)
       view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
-        insert_xml view#buffer goal.Interface.goal_ccl;
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter given_up_goals;
@@ -153,7 +154,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
       let iter goal =
-        insert_xml view#buffer goal.Interface.goal_ccl;
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter shelved_goals
@@ -166,7 +167,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
         let () = view#buffer#insert (goal_str (succ i)) in
-        insert_xml view#buffer goal.Interface.goal_ccl;
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iteri iter bg
@@ -192,7 +193,7 @@ let proof_view () =
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
 
-  object
+  let pf = object
     inherit GObj.widget view#as_widget
     val mutable goals = None
     val mutable evars = None
@@ -207,9 +208,11 @@ let proof_view () =
 
     method refresh () =
       let dummy _ () = () in
-      display (mode_tactic dummy) (view :> GText.view_skel) goals None evars
-
-    method width = Ideutils.textview_width (view :> GText.view_skel)
+      display (mode_tactic dummy) view goals None evars
   end
-
-(*     ignore (proof_buffer#add_selection_clipboard cb); *)
+  in
+  (* Is there a better way to connect the signal ? *)
+  (* Can this be done in the object constructor? *)
+  let w_cb _ = pf#refresh () in
+  ignore (view#misc#connect#size_allocate w_cb);
+  pf
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index b6eae48b3..aa01d955d 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -14,7 +14,6 @@ class type proof_view =
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
-    method width : int
   end
 
 val proof_view : unit -> proof_view
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 5f82a8898..5f80d6897 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -12,6 +12,9 @@
 
 let protocol_version = "20150913"
 
+type msg_format = Richpp of int | Ppcmds
+let msg_format = ref (Richpp 72)
+
 (** * Interface of calls to Coq by CoqIde *)
 
 open Util
@@ -92,10 +95,57 @@ let to_stateid = function
 
 let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[])
 
-let of_richpp x = Element ("richpp", [], [Richpp.repr x])
-let to_richpp xml = match xml with
-  | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x
-  | x -> raise Serialize.(Marshal_error("richpp",x))
+let of_box (ppb : Pp.block_type) = let open Pp in match ppb with
+  | Pp_hbox   i -> constructor "ppbox" "hbox"   [of_int i]
+  | Pp_vbox   i -> constructor "ppbox" "vbox"   [of_int i]
+  | Pp_hvbox  i -> constructor "ppbox" "hvbox"  [of_int i]
+  | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i]
+
+let to_box = let open Pp in
+  do_match "ppbox" (fun s args -> match s with
+      | "hbox"   -> Pp_hbox   (to_int (singleton args))
+      | "vbox"   -> Pp_vbox   (to_int (singleton args))
+      | "hvbox"  -> Pp_hvbox  (to_int (singleton args))
+      | "hovbox" -> Pp_hovbox (to_int (singleton args))
+      | x        -> raise (Marshal_error("*ppbox",PCData x))
+    )
+
+let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with
+    | Ppcmd_empty         -> constructor "ppdoc" "emtpy"  []
+    | Ppcmd_string s      -> constructor "ppdoc" "string" [of_string s]
+    | Ppcmd_glue sl       -> constructor "ppdoc" "glue"   [of_list of_pp sl]
+    | Ppcmd_box (bt,s)    -> constructor "ppdoc" "box"    [of_pair of_box of_pp (bt,s)]
+    | Ppcmd_tag (t,s)     -> constructor "ppdoc" "tag"    [of_pair of_string of_pp (t,s)]
+    | Ppcmd_print_break (i,j)
+                          -> constructor "ppdoc" "break"     [of_pair of_int of_int (i,j)]
+    | Ppcmd_force_newline -> constructor "ppdoc" "newline"   []
+    | Ppcmd_comment cmd   -> constructor "ppdoc" "comment" [of_list of_string cmd]
+
+
+let rec to_pp xpp = let open Pp in
+  Pp.unrepr @@
+  do_match "ppdoc" (fun s args -> match s with
+    | "empty"     -> Ppcmd_empty
+    | "string"    -> Ppcmd_string (to_string (singleton args))
+    | "glue"      -> Ppcmd_glue (to_list to_pp (singleton args))
+    | "box"       -> let (bt,s) = to_pair to_box to_pp (singleton args) in
+                     Ppcmd_box(bt,s)
+    | "tag"       -> let (tg,s) = to_pair to_string to_pp (singleton args) in
+                     Ppcmd_tag(tg,s)
+    | "break"     -> let (i,j)   = to_pair to_int to_int (singleton args) in
+                     Ppcmd_print_break(i, j)
+    | "newline"   -> Ppcmd_force_newline
+    | "comment"   -> Ppcmd_comment (to_list to_string (singleton args))
+    | x           -> raise (Marshal_error("*ppdoc",PCData x))
+  ) xpp
+
+let of_richpp x = Element ("richpp", [], [x])
+
+(* Run-time Selectable *)
+let of_pp (pp : Pp.std_ppcmds) =
+  match !msg_format with
+  | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp)
+  | Ppcmds        -> of_pp pp
 
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
@@ -104,7 +154,7 @@ let of_value f = function
   | None -> []
   | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
   let id = of_stateid id in
-  Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg])
+  Element ("value", ["val", "fail"] @ loc, [id; of_pp msg])
 
 let to_value f = function
 | Element ("value", attrs, l) ->
@@ -120,7 +170,7 @@ let to_value f = function
     in
     let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in
     let id = to_stateid id in
-    let msg = to_richpp msg in
+    let msg = to_pp msg    in
     Fail (id, loc, msg)
   else raise (Marshal_error("good or fail",PCData ans))
 | x -> raise (Marshal_error("value",x))
@@ -147,15 +197,15 @@ let to_evar = function
   | x -> raise (Marshal_error("evar",x))
 
 let of_goal g =
-  let hyp = of_list of_richpp g.goal_hyp in
-  let ccl = of_richpp g.goal_ccl in
+  let hyp = of_list of_pp g.goal_hyp in
+  let ccl = of_pp g.goal_ccl in
   let id = of_string g.goal_id in
   Element ("goal", [], [id; hyp; ccl])
 let to_goal = function
   | Element ("goal", [], [id; hyp; ccl]) ->
-    let hyp = to_list to_richpp hyp in
-    let ccl = to_richpp ccl in
-    let id = to_string id in
+    let hyp = to_list to_pp hyp in
+    let ccl = to_pp ccl         in
+    let id  = to_string id      in
     { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
   | x -> raise (Marshal_error("goal",x))
 
@@ -344,8 +394,8 @@ end = struct
         Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
     else
       let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-        "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^
-            Richpp.raw_print goal ^ "]" in
+        "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^
+            Pp.string_of_ppcmds goal ^ "]" in
       String.concat " " (List.map pr_goal g.fg_goals)
   let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
   let pr_status (s : status) =
@@ -631,6 +681,9 @@ let of_answer : type a. a call -> a value -> xml = function
   | PrintAst _   -> of_value (of_value_type print_ast_rty_t  )
   | Annotate _   -> of_value (of_value_type annotate_rty_t   )
 
+let of_answer msg_fmt =
+  msg_format := msg_fmt; of_answer
+
 let to_answer : type a. a call -> xml -> a value = function
   | Add _        -> to_value (to_value_type add_rty_t        )
   | Edit_at _    -> to_value (to_value_type edit_at_rty_t    )
@@ -701,10 +754,10 @@ let to_call : xml -> unknown_call =
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]"
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]"
   | Fail (id,Some(i,j),str) ->
       "FAIL "^Stateid.to_string id^
-        " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]"
+        " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with
   | Add _        -> pr_value_gen (print add_rty_t        ) value
@@ -760,7 +813,7 @@ let document to_string_fmt =
     (to_string_fmt (of_value (fun _ -> PCData "b") (Good ())));
   Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n"
     (to_string_fmt (of_value (fun _ -> PCData "b")
-      (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message"))));
+      (Fail (Stateid.initial,Some (15,34), Pp.str "error message"))));
   document_type_encoding to_string_fmt
 
 (* Moved from feedback.mli : This is IDE specific and we don't want to
@@ -787,20 +840,14 @@ let to_message_level =
 let of_message lvl loc msg =
   let lvl     = of_message_level lvl in
   let xloc    = of_option of_loc loc in
-  let content = of_richpp msg        in
+  let content = of_pp msg            in
   Xml_datatype.Element ("message", [], [lvl; xloc; content])
 
 let to_message xml = match xml with
   | Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
-      Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
+      Message(to_message_level lvl, to_option to_loc xloc, to_pp content)
   | x -> raise (Marshal_error("message",x))
 
-let is_message xml =
-  try begin match to_message xml with
-    | Message(l,c,m) -> Some (l,c,m)
-    | _              -> None
-  end with | Marshal_error _ -> None
-
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "addedaxiom", _ -> AddedAxiom
   | "processed", _ -> Processed
@@ -870,6 +917,9 @@ let of_feedback msg =
   let route = string_of_int msg.route in
   Element ("feedback", obj @ ["route",route], [id;content])
 
+let of_feedback msg_fmt =
+  msg_format := msg_fmt; of_feedback
+
 let to_feedback xml = match xml with
   | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
       id = Edit(to_edit_id id);
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 1bb998970..9cefab517 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -40,12 +40,17 @@ val abstract_eval_call : handler -> 'a call -> 'a value
 
 val protocol_version : string
 
+(** By default, we still output messages in Richpp so we are
+    compatible with 8.6, however, 8.7 aware clients will want to
+    set this to Ppcmds *)
+type msg_format = Richpp of int | Ppcmds
+
 (** * XML data marshalling *)
 
 val of_call : 'a call -> xml
 val to_call : xml -> unknown_call
 
-val of_answer : 'a call -> 'a value -> xml
+val of_answer : msg_format -> 'a call -> 'a value -> xml
 val to_answer : 'a call -> xml -> 'a value
 
 (* Prints the documentation of this module *)
@@ -57,16 +62,8 @@ val pr_call : 'a call -> string
 val pr_value : 'a value -> string
 val pr_full_value : 'a call -> 'a value -> string
 
-(** * Serialization of rich documents *)
-val of_richpp : Richpp.richpp -> Xml_datatype.xml
-val to_richpp : Xml_datatype.xml -> Richpp.richpp
-
 (** * Serializaiton of feedback  *)
-val of_feedback : Feedback.feedback -> xml
+val of_feedback : msg_format -> Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback
-val is_feedback : xml -> bool
-
-val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option
-val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
-(* val to_message : xml -> Feedback.message *)
 
+val is_feedback : xml -> bool