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.

3 files changed, 13 insertions, 12 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;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1a27d9692..87e27be69 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -473,10 +473,10 @@ GEXTEND Gram
     [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
       | IDENT "_eqn"; ":"; pat = naming_intropattern ->
         let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in
-        msg_warning (strbrk msg); Some (!@loc, pat)
+        Feedback.msg_warning (strbrk msg); Some (!@loc, pat)
       | IDENT "_eqn" ->
         let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in
-        msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
+        Feedback.msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
       | -> None ] ]
   ;
   as_name:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index df42d9084..0df15babd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -125,13 +125,13 @@ END
 
 let test_plural_form = function
   | [(_,([_],_))] ->
-      Flags.if_verbose msg_warning
+      Flags.if_verbose Feedback.msg_warning
    (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
   | _ -> ()
 
 let test_plural_form_types = function
   | [([_],_)] ->
-      Flags.if_verbose msg_warning
+      Flags.if_verbose Feedback.msg_warning
    (strbrk "Keywords Implicit Types expect more than one type")
   | _ -> ()
 
@@ -448,7 +448,7 @@ GEXTEND Gram
 	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
 	  Flags.if_verbose
-            msg_warning (strbrk "Include Type is deprecated; use Include instead");
+            Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead");
           VernacInclude(e::l) ] ]
   ;
   export_token:
@@ -667,7 +667,7 @@ GEXTEND Gram
      (* moved there so that camlp5 factors it with the previous rule *)
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
-        msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
+       Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
         VernacArgumentsScope (qid,scl)
 
       (* Implicit *)
@@ -675,7 +675,7 @@ GEXTEND Gram
 	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   Flags.if_verbose
-             msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
+            Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
 	   VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->