Feedback cleanup

This patch splits pretty printing representation from IO operations.

- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.

The patch continues work initiated for 8.5 and has the following effects:

- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
  `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
  `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
  used instead.

- Feedback provides different backends to handle output, currently,
  `stdout`, `emacs` and CoqIDE backends are provided.

- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
  gone.

- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
  mix.

Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.

1 files changed, 5 insertions, 5 deletions

diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 9d159be64..246b00da4 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -29,13 +29,13 @@ and translate_field prefix mp env acc (l,x) =
      let con = make_con mp empty_dirpath l in
      (if !Flags.debug then
 	let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_constant_field (pre_env env) prefix con acc cb
   | SFBmind mb ->
      (if !Flags.debug then
 	let id = mb.mind_packets.(0).mind_typename in
 	let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_mind_field prefix mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
@@ -43,7 +43,7 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
@@ -51,11 +51,11 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
-  if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
+  if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library...");
   match mod_expr with
   | NoFunctor struc ->
       let env = add_structure mp struc empty_delta_resolver env in