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, 8 insertions, 8 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4296b73ab..5b92e9554 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -73,20 +73,20 @@ let call_compiler ml_filename =
     ::"-w"::"a"
     ::include_dirs
     @ ["-impl"; ml_filename] in
-  if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
+  if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
       | Unix.WEXITED n ->
-         Pp.(msg_warning (str "command exited with status " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
       | Unix.WSIGNALED n ->
-         Pp.(msg_warning (str "command killed by signal " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
       | Unix.WSTOPPED n ->
-         Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+         Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    Pp.(msg_warning (str (Unix.error_message e)));
+    Feedback.msg_warning Pp.(str (Unix.error_message e));
     false, link_filename
 
 let compile fn code =
@@ -120,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds =
     begin
       let msg = "Cannot find native compiler file " ^ f in
       if fatal then Errors.error msg
-      else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
     end
   else
   (try
@@ -129,8 +129,8 @@ let call_linker ?(fatal=true) prefix f upds =
    with Dynlink.Error e as exn ->
      let exn = Errors.push exn in
      let msg = "Dynlink error, " ^ Dynlink.error_message e in
-     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
-     else if !Flags.debug then Pp.msg_debug (Pp.str msg));
+     if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
+     else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =