Merge PR #1075: Re-enable checker error messages

2 files changed, 39 insertions, 1 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 67b812133..247a98e63 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -365,10 +365,48 @@ let parse_args argv =
 (* To prevent from doing the initialization twice *)
 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 ();
     try
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3c9e1cac5..63e28448f 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -25,7 +25,7 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
+  Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ prcon kn);
   (** [env'] contains De Bruijn universe variables *)
   let env' =
     match cb.const_universes with