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.

14 files changed, 131 insertions, 128 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index a9c53b4d4..10e9b30be 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -262,7 +262,7 @@ let add_new_coercion_core coef stre poly source target isid =
   in
   check_source (Some cls);
   if not (uniform_cond (llp-ind) lvs) then
-    msg_warning (explain_coercion_error coef NotUniform);
+    Feedback.msg_warning (explain_coercion_error coef NotUniform);
   let clt =
     try
       get_target tg ind
@@ -310,7 +310,7 @@ let add_coercion_hook poly local ref =
   in
   let () = try_add_new_coercion ref stre poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
-  Flags.if_verbose msg_info msg
+  Flags.if_verbose Feedback.msg_info msg
 
 let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5865fec06..f0f678e08 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -119,7 +119,7 @@ let interp_definition pl bl p red_option c ctypopt =
           impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
-	then msg_warning
+	then Feedback.msg_warning
           (strbrk "Implicit arguments declaration relies on type." ++ spc () ++
 	   strbrk "The term declares more implicits than the type here.");
         let vars = Univ.LSet.union (Universes.universes_of_constr body) 
@@ -140,7 +140,7 @@ let get_locality id = function
 | Discharge ->
   (** If a Let is defined outside a section, then we consider it as a local definition *)
   let msg = pr_id id ++ strbrk " is declared as a local definition" in
-  let () = msg_warning msg in
+  let () = Feedback.msg_warning msg in
   true
 | Local -> true
 | Global -> false
@@ -171,7 +171,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = if Pfedit.refining () then
       let msg = strbrk "Section definition " ++
         pr_id ident ++ strbrk " is not visible from current goals" in
-      msg_warning msg
+      Feedback.msg_warning msg
     in
     gr
   | Discharge | Local | Global ->
@@ -217,7 +217,7 @@ match local with
   let () = assumption_message ident in
   let () =
     if is_verbose () && Pfedit.refining () then
-    msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
+    Feedback.msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
     strbrk " is not visible from current goals")
   in
   let r = VarRef ident in
@@ -706,7 +706,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
 		constrimpls)
       impls;
   let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
-  if_verbose msg_info (minductive_message warn_prim names);
+  if_verbose Feedback.msg_info (minductive_message warn_prim names);
   if mie.mind_entry_private == None
   then declare_default_schemes mind;
   mind
@@ -799,7 +799,7 @@ let check_mutuality env isfix fixl =
   let po = partial_order Id.equal preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
     | (x,Inr xge)::(y,Inr yge)::rest ->
-	msg_warning (non_full_mutual_message x xge y yge isfix rest)
+	Feedback.msg_warning (non_full_mutual_message x xge y yge isfix rest)
     | _ -> ()
 
 type structured_fixpoint_expr = {
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b81c8da71..e4975fa31 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -36,7 +36,7 @@ let load_rcfile() =
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
-	  let warn x = msg_warning (str x) in
+	  let warn x = Feedback.msg_warning (str x) in
 	  let inferedrc = List.find CUnix.file_readable_p [
 	    Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
 	    Envars.xdg_config_home warn / rcdefaultname;
@@ -52,10 +52,10 @@ let load_rcfile() =
 	*)
     with reraise ->
       let reraise = Errors.push reraise in
-      let () = msg_info (str"Load of rcfile failed.") in
+      let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
   else
-    Flags.if_verbose msg_info (str"Skipping rcfile loading.")
+    Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.")
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
@@ -78,7 +78,7 @@ let push_ml_include s = ml_includes := s :: !ml_includes
 let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
-  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in
+  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
   let coqpath = Envars.coqpath in
   let coq_root = Names.DirPath.make [Nameops.coq_root] in
     (* NOTE: These directories are searched from last to first *)
@@ -135,6 +135,6 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
+    Feedback.msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
     Flags.V8_2
   | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 040c33924..c8879963e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,6 +13,8 @@ open Flags
 open Vernac
 open Pcoq
 
+let top_stderr x = msg_with !Pp_control.err_ft x
+
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
 
@@ -59,7 +61,7 @@ let prompt_char ic ibuf count =
     | ll::_ -> Int.equal ibuf.len ll
     | [] -> Int.equal ibuf.len 0
   in
-  if bol && not !print_emacs then msgerr (str (ibuf.prompt()));
+  if bol && not !print_emacs then top_stderr (str (ibuf.prompt()));
   try
     let c = input_char ic in
     if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -310,23 +312,23 @@ let read_sentence () =
 *)
 
 let do_vernac () =
-  msgerrnl (mt ());
-  if !print_emacs then msgerr (str (top_buffer.prompt()));
+  top_stderr (fnl());
+  if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
     Vernac.eval_expr (read_sentence ())
   with
     | End_of_input | Errors.Quit ->
-        msgerrnl (mt ()); pp_flush(); raise Errors.Quit
+        top_stderr (fnl ()); raise Errors.Quit
     | Errors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise Errors.Drop
-        else ppnl (str"Error: There is no ML toplevel." ++ fnl ())
+        else Feedback.msg_error (str"There is no ML toplevel.")
     | any ->
         let any = Errors.push any in
         Format.set_formatter_out_channel stdout;
         let msg = print_toplevel_error any ++ fnl () in
         pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
-        pp_flush ()
+        flush_all ()
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -354,7 +356,7 @@ let rec loop () =
     | Errors.Drop -> ()
     | Errors.Quit -> exit 0
     | any ->
-      msgerrnl (str"Anomaly: main loop exited with exception: " ++
+      Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
                 str (Printexc.to_string any) ++
                 fnl() ++ str"Please report.");
       loop ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c4222b330..869f6bb93 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -31,10 +31,10 @@ let get_version_date () =
 
 let print_header () =
   let (ver,rev) = get_version_date () in
-  ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
-  pp_flush ()
+  Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
+  flush_all ()
 
-let warning s = with_option Flags.warn msg_warning (strbrk s)
+let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s)
 
 let toploop = ref None
 
@@ -61,7 +61,8 @@ let init_color () =
     match colors with
     | None ->
       (** Default colors *)
-      Ppstyle.init_color_output ()
+      Ppstyle.init_color_output ();
+      Feedback.set_logger Feedback.color_terminal_logger
     | Some "" ->
       (** No color output *)
       ()
@@ -69,7 +70,8 @@ let init_color () =
       (** Overwrite all colors *)
       Ppstyle.clear_styles ();
       Ppstyle.parse_config s;
-      Ppstyle.init_color_output ()
+      Ppstyle.init_color_output ();
+      Feedback.set_logger Feedback.color_terminal_logger
   end
 
 let toploop_init = ref begin fun x ->
@@ -95,8 +97,8 @@ let memory_stat = ref false
 let print_memory_stat () =
   begin (* -m|--memory from the command-line *)
     if !memory_stat then
-    ppnl
-      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes");
+    Feedback.msg_notice
+      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ());
   end;
   begin
     (* operf-macro interface:
@@ -141,7 +143,7 @@ let remove_top_ml () = Mltop.remove ()
 
 let inputstate = ref ""
 let set_inputstate s =
-  let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
+  let () = Feedback.msg_warning (str "The inputstate option is deprecated and discouraged.") in
   inputstate:=s
 let inputstate () =
   if not (String.is_empty !inputstate) then
@@ -150,7 +152,7 @@ let inputstate () =
 
 let outputstate = ref ""
 let set_outputstate s =
-  let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
+  let () = Feedback.msg_warning (str "The outputstate option is deprecated and discouraged.") in
   outputstate:=s
 let outputstate () =
   if not (String.is_empty !outputstate) then
@@ -243,7 +245,7 @@ let set_emacs () =
   if not (Option.is_empty !toploop) then
     error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
-  Pp.make_pp_emacs ();
+  Feedback.(set_logger emacs_logger);
   Vernacentries.qed_display_script := false;
   color := `OFF
 
@@ -646,7 +648,7 @@ let init_toplevel arglist =
   if !batch_mode then begin
     flush_all();
     if !output_context then
-      Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
+      Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
     Profile.print_profile ();
     exit 0
   end
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 367425546..f995a390c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -150,7 +150,7 @@ let alarm what internal msg =
   | UserAutomaticRequest
   | InternalTacticRequest ->
     (if debug then
-      msg_warning
+      Feedback.msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
   | _ -> Some msg
 
@@ -303,7 +303,7 @@ let declare_congr_scheme ind =
     then
       ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
     else
-      msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
+      Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
   end
 
 let declare_sym_scheme ind =
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index ef789aa5c..c4c891b89 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -35,7 +35,7 @@ let enforce_locality_full locality_flag local =
 	Errors.error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
-          Pp.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
+          Feedback.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
 	  Some true
 	end else
 	None
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
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index d0fa7a80c..36c16208c 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -146,7 +146,7 @@ let dir_ml_load s =
 let dir_ml_use s =
   match !load with
     | WithTop t -> t.use_file s
-    | _ -> msg_warning (str "Cannot access the ML compiler")
+    | _ -> Feedback.msg_warning (str "Cannot access the ML compiler")
 
 (* Adds a path to the ML paths *)
 let add_ml_dir s =
@@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path =
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
-    msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
+    Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
 let add_rec_path ~unix_path ~coq_root ~implicit =
@@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let () = List.iter add dirs in
     Loadpath.add_load_path unix_path ~implicit coq_root
   else
-    msg_warning (str "Cannot open " ++ str unix_path)
+    Feedback.msg_warning (str "Cannot open " ++ str unix_path)
 
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
@@ -324,10 +324,10 @@ let if_verbose_load verb f name ?path fname =
     let info = str "[Loading ML file " ++ str fname ++ str " ..." in
     try
       let path = f name ?path fname in
-      msg_info (info ++ str " done]");
+      Feedback.msg_info (info ++ str " done]");
       path
     with reraise ->
-      msg_info (info ++ str " failed]");
+      Feedback.msg_info (info ++ str " failed]");
       raise reraise
 
 (** Load a module for the first time (i.e. dynlink it)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 54baa5e3c..dbc3ccaac 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -24,7 +24,7 @@ let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
 let trace s =
-  if !Flags.debug then msg_debug s
+  if !Flags.debug then Feedback.msg_debug s
   else ()
 
 let succfix (depth, fixrels) =
@@ -731,11 +731,11 @@ type progress =
 let obligations_message rem =
   if rem > 0 then
     if Int.equal rem 1 then
-      Flags.if_verbose msg_info (int rem ++ str " obligation remaining")
+      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining")
     else
-      Flags.if_verbose msg_info (int rem ++ str " obligations remaining")
+      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining")
   else
-    Flags.if_verbose msg_info (str "No more obligations remaining")
+    Flags.if_verbose Feedback.msg_info (str "No more obligations remaining")
 
 let update_obls prg obls rem =
   let prg' = { prg with prg_obligations = (obls, rem) } in
@@ -992,7 +992,7 @@ and try_solve_obligations n tac =
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
 and auto_solve_obligations n ?oblset tac : progress =
-  Flags.if_verbose msg_info (str "Solving obligations automatically...");
+  Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically...");
   try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
 
 open Pp
@@ -1000,13 +1000,13 @@ let show_obligations_of_prg ?(msg=true) prg =
   let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
   let showed = ref 5 in
-    if msg then msg_info (int rem ++ str " obligation(s) remaining: ");
+    if msg then Feedback.msg_info (int rem ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x ->
 		   match x.obl_body with
 		   | None ->
 		       if !showed > 0 then (
 			 decr showed;
-			 msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+			 Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
 				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
 				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
 					    str "." ++ fnl ())))
@@ -1035,12 +1035,12 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
   let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
-    Flags.if_verbose msg_info (info ++ str ".");
+    Flags.if_verbose Feedback.msg_info (info ++ str ".");
     let cst = declare_definition prg in
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
       progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d12b5ee8e..0c3bd953c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -196,7 +196,7 @@ let warning_or_error coe indsp err =
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then errorlabstrm "structure" st;
-  Flags.if_verbose msg_warning (hov 0 st)
+  Flags.if_verbose Feedback.msg_warning (hov 0 st)
 
 type field_status =
   | NoProjection of Name.t
@@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	| Some None | None -> false
       in
 	if not is_primitive then 
-	  Flags.if_verbose msg_warning
+	  Flags.if_verbose Feedback.msg_warning
 	    (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ 
 		      str" could not be defined as a primitive record"));
 	is_primitive
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 64225a644..1c3f0d997 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -119,8 +119,7 @@ let verbose_phrase verbch loc =
 	let s = String.create len in
         seek_in ch (fst loc);
         really_input ch s 0 len;
-        ppnl (str s);
-        pp_flush()
+        Feedback.msg_notice (str s ++ fnl ())
     | None -> ()
 
 exception End_of_input
@@ -152,9 +151,9 @@ let pr_new_syntax loc ocom =
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
   if !beautify_file then
-    msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
-    msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+    Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
@@ -193,14 +192,15 @@ let display_cmd_header loc com =
     with e -> str (Printexc.to_string e) in
   let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
   in
-  Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
-	 str " [" ++ str cmd ++ str "] ");
-  Pp.flush_all ()
+  Feedback.msg_notice
+    (str "Chars " ++ int start ++ str " - " ++ int stop ++
+     str " [" ++ str cmd ++ str "] ")
+
 
 let rec vernac_com verbose checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
-	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
 	let st = save_translator_coqdoc () in
@@ -248,8 +248,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com verbosely checknav loc_ast;
-      pp_flush ()
+      vernac_com verbosely checknav loc_ast
     done
   with any ->   (* whatever the exception *)
     let (e, info) = Errors.push any in
@@ -294,7 +293,7 @@ let load_vernac verb file =
 let ensure_v f =
   if Filename.check_suffix f ".v" then f
   else begin
-    msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
+    Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
     expanded to \"" ++ str f ++ str ".v\"");
     f ^ ".v"
   end
@@ -304,7 +303,7 @@ let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
     if not (List.is_empty pfs) then
-      (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+      (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in
   match !Flags.compilation_mode with
   | BuildVo ->
       let long_f_dot_v = ensure_v f in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 23755dac1..222b7d3df 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -57,7 +57,7 @@ let show_proof () =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   let p = Proof_global.give_me_the_proof () in
   let pprf = Proof.partial_proof p in
-  msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
+  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
 
 let show_node () =
   (* spiwack: I'm have little clue what this function used to do. I deactivated it, 
@@ -65,22 +65,22 @@ let show_node () =
   ()
 
 let show_thesis () =
-     msg_error (anomaly (Pp.str "TODO") )
+     Feedback.msg_error (anomaly (Pp.str "TODO") )
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
   let pfts = get_pftreestate () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
-  msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
+  Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
 
 let show_universes () =
   let pfts = get_pftreestate () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
-    msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
-    msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
+    Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
+    Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
 
 let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)
@@ -91,11 +91,10 @@ let enable_goal_printing = ref true
 let print_subgoals () =
   if !enable_goal_printing && is_verbose ()
   then begin
-    msg_notice (pr_open_subgoals ())
+    Feedback.msg_notice (pr_open_subgoals ())
   end
 
 let try_print_subgoals () =
-  Pp.flush_all();
   try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()
 
 
@@ -109,10 +108,10 @@ let show_intro all =
     let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
     if all then
       let lid = Tactics.find_intro_names l gl in
-      msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
+      Feedback.msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
     else if not (List.is_empty l) then
       let n = List.last l in
-      msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+      Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
   end
 
 (** Prepare a "match" template for a given inductive type.
@@ -153,7 +152,7 @@ let show_match id =
   let pr_branch l =
     str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
   in
-  msg_notice (v 1 (str "match # with" ++ fnl () ++
+  Feedback.msg_notice (v 1 (str "match # with" ++ fnl () ++
 	    prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()))
 
 (* "Print" commands *)
@@ -194,23 +193,23 @@ let print_module r =
     let globdir = Nametab.locate_dir qid in
       match globdir with
 	  DirModule (dirpath,(mp,_)) ->
-	    msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
+	    Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
 	| _ -> raise Not_found
   with
-      Not_found -> msg_error (str"Unknown Module " ++ pr_qualid qid)
+      Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)
 
 let print_modtype r =
   let (loc,qid) = qualid_of_reference r in
   try
     let kn = Nametab.locate_modtype qid in
-    msg_notice (Printmod.print_modtype kn)
+    Feedback.msg_notice (Printmod.print_modtype kn)
   with Not_found ->
     (* Is there a module of this name ? If yes we display its type *)
     try
       let mp = Nametab.locate_module qid in
-      msg_notice (Printmod.print_module false mp)
+      Feedback.msg_notice (Printmod.print_module false mp)
     with Not_found ->
-      msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
+      Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
 
 let print_namespace ns =
   let ns = List.rev (Names.DirPath.repr ns) in
@@ -279,7 +278,7 @@ let print_namespace ns =
         acc
     ) constants (str"")
   in
-  msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
+  Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
 
 let print_strategy r =
   let open Conv_oracle in
@@ -309,7 +308,7 @@ let print_strategy r =
       else str "Constant strategies" ++ fnl () ++
         hov 0 (prlist_with_sep fnl pr_strategy cst_lvl)
     in
-    msg_notice (var_msg ++ cst_msg)
+    Feedback.msg_notice (var_msg ++ cst_msg)
   | Some r ->
     let r = Smartlocate.smart_global r in
     let key = match r with
@@ -318,7 +317,7 @@ let print_strategy r =
     | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable"
     in
     let lvl = get_strategy oracle key in
-    msg_notice (pr_strategy (r, lvl))
+    Feedback.msg_notice (pr_strategy (r, lvl))
 
 let dump_universes_gen g s =
   let output = open_out s in
@@ -352,7 +351,7 @@ let dump_universes_gen g s =
   try
     UGraph.dump_universes output_constraint g;
     close ();
-    msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
+    Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
   with reraise ->
     let reraise = Errors.push reraise in
     close ();
@@ -367,11 +366,11 @@ let locate_file f =
 
 let msg_found_library = function
   | Library.LibLoaded, fulldir, file ->
-      msg_info (hov 0
+      Feedback.msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
 	 str file))
   | Library.LibInPath, fulldir, file ->
-      msg_info (hov 0
+      Feedback.msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
 
 let err_unmapped_library loc ?from qid =
@@ -506,7 +505,7 @@ let vernac_exact_proof c =
      called only at the begining of a proof. *)
   let status = by (Tactics.exact_proof c) in
   save_proof (Vernacexpr.(Proved(Opaque None,None)));
-  if not status then Pp.feedback Feedback.AddedAxiom
+  if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =
   let local = enforce_locality_exp locality local in
@@ -518,7 +517,7 @@ let vernac_assumption locality poly (local, kind) l nl =
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
   let status = do_assumptions kind nl l in
-  if not status then Pp.feedback Feedback.AddedAxiom
+  if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_record k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
@@ -636,7 +635,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
       id binders_ast (Enforce mty_ast) []
   in
   Dumpglob.dump_moddef loc mp "mod";
-  if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared");
+  if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -657,7 +656,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
            export id binders_ast mty_ast_o
        in
        Dumpglob.dump_moddef loc mp "mod";
-       if_verbose msg_info
+       if_verbose Feedback.msg_info
          (str "Interactive Module " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
@@ -675,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 	   id binders_ast mty_ast_o mexpr_ast_l
        in
        Dumpglob.dump_moddef loc mp "mod";
-       if_verbose msg_info
+       if_verbose Feedback.msg_info
 	 (str "Module " ++ pr_id id ++ str " is defined");
        Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
          export
@@ -683,7 +682,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref loc mp "mod";
-  if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined");
+  if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -704,7 +703,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
            id binders_ast mty_sign
        in
        Dumpglob.dump_moddef loc mp "modtype";
-       if_verbose msg_info
+       if_verbose Feedback.msg_info
 	 (str "Interactive Module Type " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
@@ -723,13 +722,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	    id binders_ast mty_sign mty_ast_l
         in
         Dumpglob.dump_moddef loc mp "modtype";
-	if_verbose msg_info
+	if_verbose Feedback.msg_info
 	  (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref loc mp "modtype";
-  if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+  if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_module_ast l
@@ -797,7 +796,7 @@ let vernac_coercion locality poly local ref qids qidt =
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
   Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
-  if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
+  if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion locality poly local id qids qidt =
   let local = enforce_locality locality local in
@@ -813,7 +812,7 @@ let vernac_instance abst locality poly sup inst props pri =
   ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
 
 let vernac_context poly l =
-  if not (Classes.context poly l) then Pp.feedback Feedback.AddedAxiom
+  if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_declare_instances locality ids pri =
   let glob = not (make_section_locality locality) in
@@ -869,7 +868,7 @@ let vernac_set_used_variables e =
 (* Auxiliary file management *)
 
 let expand filename =
-  Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename
+  Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
 
 let vernac_add_loadpath implicit pdir ldiropt =
   let pdir = expand pdir in
@@ -889,13 +888,13 @@ let vernac_declare_ml_module locality l =
   Mltop.declare_ml_modules local (List.map expand l)
 
 let vernac_chdir = function
-  | None -> msg_notice (str (Sys.getcwd()))
+  | None -> Feedback.msg_notice (str (Sys.getcwd()))
   | Some path ->
       begin
 	try Sys.chdir (expand path)
-	with Sys_error err -> msg_warning (str "Cd failed: " ++ str err)
+	with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err)
       end;
-      if_verbose msg_info (str (Sys.getcwd()))
+      if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
 
 (********************)
@@ -1068,7 +1067,7 @@ let vernac_declare_arguments locality r l nargs flags =
           some_scopes_specified ||
           some_simpl_flags_specified) &&
      no_flags then
-    msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
+    Feedback.msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
 
 
 let default_env () = {
@@ -1423,7 +1422,7 @@ let vernac_check_may_eval redexp glopt rc =
     | None ->
         let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
-	msg_notice (print_judgment env sigma' j ++
+	Feedback.msg_notice (print_judgment env sigma' j ++
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
                     Printer.pr_universe_ctx sigma uctx)
     | Some r ->
@@ -1434,7 +1433,7 @@ let vernac_check_may_eval redexp glopt rc =
           let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in
           c
         in
-	msg_notice (print_eval redfun env sigma' rc j)
+	Feedback.msg_notice (print_eval redfun env sigma' rc j)
 
 let vernac_declare_reduction locality s r =
   let local = make_locality locality in
@@ -1450,7 +1449,7 @@ let vernac_global_check c =
   let senv = Safe_typing.add_constraints cstrs senv in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
-    msg_notice (print_safe_judgment env sigma j)
+    Feedback.msg_notice (print_safe_judgment env sigma j)
 
 
 let get_nth_goal n =
@@ -1487,7 +1486,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
     | NoHyp | Not_found -> print_about ref_or_by_not
 
 	       
-let vernac_print = function
+let vernac_print = let open Feedback in function
   | PrintTables -> msg_notice (print_tables ())
   | PrintFullContext-> msg_notice (print_full_context_typ ())
   | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
@@ -1586,6 +1585,7 @@ let vernac_search s gopt r =
     | Some g -> snd (Pfedit.get_goal_context g) , Some g
   in
   let get_pattern c = snd (intern_constr_pattern env c) in
+  let open Feedback in
   match s with
   | SearchPattern c ->
       msg_notice (Search.search_pattern gopt (get_pattern c) r)
@@ -1596,8 +1596,8 @@ let vernac_search s gopt r =
   | SearchAbout sl ->
      msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r)
 
-let vernac_locate = function
-  | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
+let vernac_locate = let open Feedback in function
+  | LocateAny (AN qid)  -> msg_notice (print_located_qualid qid)
   | LocateTerm (AN qid) -> msg_notice (print_located_term qid)
   | LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *)
   | LocateTerm (ByNotation (_, ntn, sc)) ->
@@ -1640,7 +1640,7 @@ let vernac_unfocus () =
 let vernac_unfocused () =
   let p = Proof_global.give_me_the_proof () in
   if Proof.unfocused p then
-    msg_notice (str"The proof is indeed fully unfocused.")
+    Feedback.msg_notice (str"The proof is indeed fully unfocused.")
   else
     error "The proof is not fully unfocused."
 
@@ -1668,7 +1668,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) =
   Proof_global.simple_with_current_proof (fun _ p ->
     Proof_global.Bullet.put p bullet)
 
-let vernac_show = function
+let vernac_show = let open Feedback in function
   | ShowGoal goalref ->
     let info = match goalref with
       | OpenSubgoals -> pr_open_subgoals ()
@@ -1706,7 +1706,7 @@ let vernac_check_guard () =
     with UserError(_,s) ->
       (str ("Condition violated: ") ++s)
   in
-  msg_notice message
+  Feedback.msg_notice message
 
 exception End_of_input
 
@@ -1717,7 +1717,7 @@ let vernac_load interp fname =
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
-    Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+    Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in
   let input =
     let longfname = Loadpath.locate_file fname in
@@ -1849,15 +1849,15 @@ let interp ?proof ~loc locality poly c =
   | VernacSearch (s,g,r) -> vernac_search s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
-  | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
+  | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm")
-  | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm")
-  | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm")
-  | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm")
-  | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm")
-  | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm")
+  | VernacAbort id -> Feedback.msg_warning (str "VernacAbort not handled by Stm")
+  | VernacAbortAll -> Feedback.msg_warning (str "VernacAbortAll not handled by Stm")
+  | VernacRestart -> Feedback.msg_warning (str "VernacRestart not handled by Stm")
+  | VernacUndo _ -> Feedback.msg_warning (str "VernacUndo not handled by Stm")
+  | VernacUndoTo _ -> Feedback.msg_warning (str "VernacUndoTo not handled by Stm")
+  | VernacBacktrack _ -> Feedback.msg_warning (str "VernacBacktrack not handled by Stm")
   
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -1991,7 +1991,7 @@ let with_fail b f =
       | HasNotFailed ->
           errorlabstrm "Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if is_verbose () || !test_mode || !ide_slave then msg_info
+          if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end
@@ -2016,7 +2016,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacRedirect (s, (_,v)) ->
-         Pp.with_output_to_file s (aux false) v
+         Feedback.with_output_to_file s (aux false) v
     | VernacTime (_,v) ->
         System.with_time !Flags.time
           (aux ?locality ?polymorphism isprogcmd) v;
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 7fbd2b119..1116a3104 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -55,7 +55,7 @@ let call ?locality (opn,converted_args) =
       | Egramml.GramNonTerminal _ -> str "_"
       in
       let pr = pr_sequence pr_gram rules in
-      msg_warning (str "Deprecated vernacular command: " ++ pr)
+      Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr)
     in
     loc:= "Checking arguments";
     let hunk = callback converted_args in
@@ -68,5 +68,5 @@ let call ?locality (opn,converted_args) =
     | reraise ->
         let reraise = Errors.push reraise in
         if !Flags.debug then
-	  msg_debug (str"Vernac Interpreter " ++ str !loc);
+	  Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc);
         iraise reraise