1 files changed, 13 insertions, 11 deletions
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