Merge PR#530: [toplevel] Remove exception error printer in favor of feedback printer.

2 files changed, 14 insertions, 17 deletions

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e3c0a1709..ee5536692 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -108,7 +108,7 @@ end
 
 type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
 
-let msgnl_with fmt strm =
+let msgnl_with ?pre_hdr fmt strm =
   pp_with fmt (strm ++ fnl ());
   Format.pp_print_flush fmt ()
 
@@ -138,19 +138,17 @@ let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
 let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
 let  ann_hdr = tag Tag.error   (str "Anomaly:") ++ spc ()
 
-let make_body quoter info ?loc s =
-  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
-  quoter (hov 0 (loc ++ info ++ s))
+let make_body quoter info ?pre_hdr s =
+  pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s))
 
 (* Generic logger *)
-let gen_logger dbg err ?loc level msg = match level with
-  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?loc msg)
-  | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg)
-  (* XXX: What to do with loc here? *)
-  | Notice  -> msgnl_with !std_ft msg
+let gen_logger dbg err ?pre_hdr level msg = match level with
+  | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?pre_hdr msg)
+  | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
+  | Notice  -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?loc msg)
+               msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?pre_hdr msg)
 
 (** Standard loggers *)
 
@@ -159,8 +157,8 @@ let gen_logger dbg err ?loc level msg = match level with
 *)
 let std_logger_cleanup = ref (fun () -> ())
 
-let std_logger ?loc level msg =
-  gen_logger (fun x -> x) (fun x -> x) ?loc level msg;
+let std_logger ?pre_hdr level msg =
+  gen_logger (fun x -> x) (fun x -> x) ?pre_hdr level msg;
   !std_logger_cleanup ()
 
 (** Color logging. Moved from Ppstyle, it may need some more refactoring  *)
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 0e122f46e..909dd7077 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -40,10 +40,9 @@ val get_margin : unit -> int option
 val err_hdr : Pp.std_ppcmds
 val ann_hdr : Pp.std_ppcmds
 
-(** Console display of feedback *)
-val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
-
-val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit
+(** Console display of feedback, we may add some location information *)
+val std_logger   : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
+val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
 
 val init_color_output : unit -> unit
 val clear_styles : unit -> unit