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/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d60c73939..52117f13f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -568,7 +568,7 @@ let is_not_small_constr = function
 let rec define_keywords_aux = function
   | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
       when is_not_small_constr e ->
-      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+      Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       CLexer.add_keyword k;
       n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
@@ -577,7 +577,7 @@ let rec define_keywords_aux = function
   (* Ensure that IDENT articulation terminal symbols are keywords *)
 let define_keywords = function
   | GramConstrTerminal(IDENT k)::l ->
-      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+      Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       CLexer.add_keyword k;
       GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
@@ -855,12 +855,12 @@ let check_rule_productivity l =
 let is_not_printable onlyparse noninjective = function
 | NVar _ ->
   let () = if not onlyparse then
-    msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
+    Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
   in
   true
 | _ ->
   if not onlyparse && noninjective then
-    let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
+    let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
     true
   else onlyparse
 
@@ -886,7 +886,7 @@ let find_precedence lev etyps symbols =
 	| ETName | ETBigint | ETReference ->
             begin match lev with
             | None ->
-	      ([msg_info,strbrk "Setting notation at level 0."],0)
+	      ([Feedback.msg_info,strbrk "Setting notation at level 0."],0)
             | Some 0 ->
               ([],0)
             | _ ->
@@ -904,7 +904,7 @@ let find_precedence lev etyps symbols =
 	else [],Option.get lev)
   | Terminal _ when last_is_terminal () ->
       if Option.is_empty lev then
-	([msg_info,strbrk "Setting notation at level 0."], 0)
+	([Feedback.msg_info,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
   | _ ->
       if Option.is_empty lev then error "Cannot determine the level.";
@@ -931,7 +931,7 @@ let remove_curly_brackets l =
             (match next' with
               | Terminal "}" as t2 :: l'' as l1 ->
                   if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
-                    msg_warning (strbrk "Skipping spaces inside curly brackets");
+                    Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets");
                   if deb && List.is_empty l'' then [t1;x;t2] else begin
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
@@ -976,7 +976,7 @@ let compute_pure_syntax_data df mods =
   let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
   let msgs =
     if onlyparse then
-      (msg_warning,
+      (Feedback.msg_warning,
       strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
   msgs, sy_data, extra