[feedback] Helper to print feedback messages in the console.

This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.

1 files changed, 1 insertions, 36 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 247a98e63..e960a55fd 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -367,46 +367,11 @@ let initialized = ref false
 
 (* XXX: At some point we need to either port the checker to use the
    feedback system or to remove its use completely. *)
-let init_feedback_listener () =
-  let open Format in
-  let pp_lvl fmt lvl = let open Feedback in match lvl with
-    | Error   -> fprintf fmt "Error: "
-    | Info    -> fprintf fmt "Info: "
-    | Debug   -> fprintf fmt "Debug: "
-    | Warning -> fprintf fmt "Warning: "
-    | Notice  -> fprintf fmt ""
-  in
-  let pp_loc fmt loc = let open Loc in match loc with
-    | None     -> fprintf fmt ""
-    | Some loc ->
-      let where =
-        match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in
-      fprintf fmt "\"%s\", line %d, characters %d-%d:@\n"
-        where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in
-  let checker_feed (fb : Feedback.feedback) = let open Feedback in
-  match fb.contents with
-  | Processed   -> ()
-  | Incomplete  -> ()
-  | Complete    -> ()
-  | ProcessingIn _ -> ()
-  | InProgress _ -> ()
-  | WorkerStatus (_,_) -> ()
-  | AddedAxiom  -> ()
-  | GlobRef (_,_,_,_,_) -> ()
-  | GlobDef (_,_,_,_) -> ()
-  | FileDependency (_,_) -> ()
-  | FileLoaded (_,_) -> ()
-  | Custom (_,_,_) -> ()
-  (* Re-enable when we switch back to feedback-based error printing *)
-  | Message (lvl,loc,msg) ->
-    Format.eprintf "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg
-  in ignore(Feedback.add_feeder checker_feed)
-
 let init_with_argv argv =
   if not !initialized then begin
     initialized := true;
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-    init_feedback_listener ();
+    let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
     try
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;