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, 6 insertions, 5 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 8b8b38c34..9a7aeaf0c 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -199,7 +199,7 @@ let check_keyword str =
 let check_keyword_to_add s =
   try check_keyword s
   with Error.E (UnsupportedUnicode unicode) ->
-    Flags.if_verbose msg_warning
+    Flags.if_verbose Feedback.msg_warning
       (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
                                which will not be parsable." s unicode))
 
@@ -322,7 +322,7 @@ let rec string in_comments bp len = parser
         | [< '')'; s >] ->
             let () = match in_comments with
             | Some 0 ->
-                msg_warning
+                Feedback.msg_warning
                   (strbrk
                      "Not interpreting \"*)\" as the end of current \
                       non-terminated comment because it occurs in a \
@@ -389,9 +389,10 @@ let comment_stop ep =
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
-          msgerrnl(str "No begin location for comment '"
-                   ++ str current_s ++str"' ending at  "
-                   ++ int ep);
+          Feedback.msg_notice
+            (str "No begin location for comment '"
+             ++ str current_s ++str"' ending at  "
+             ++ int ep);
           ep-1 in
     Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
   Buffer.clear current;