2 files changed, 30 insertions, 4 deletions

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index c25dd55fb..a1835959c 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -260,6 +260,29 @@ let init_color_output () =
  *)
 let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
 
+
+(* This is specific to the toplevel *)
+let pr_loc loc =
+  if Loc.is_ghost loc then str"<unknown>"
+  else
+    let fname = loc.Loc.fname in
+    if CString.equal fname "" then
+      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
+	   str"-" ++ int loc.ep ++ str":")
+    else
+      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+	   str", line " ++ int loc.line_nb ++ str", characters " ++
+	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+	   str":")
+
+let print_err_exn ?extra any =
+  let (e, info) = CErrors.push any in
+  let loc = Loc.get_loc info in
+  let msg_loc = pr_loc (Option.default Loc.ghost loc) in
+  let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in
+  let msg = CErrors.iprint (e, info) ++ fnl () in
+  std_logger ~pre_hdr Feedback.Error msg
+
 (* Output to file, used only in extraction so a candidate for removal *)
 let ft_logger old_logger ft ?loc level mesg =
   let id x = x in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 909dd7077..6c8e0ae2f 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -36,19 +36,22 @@ val get_depth_boxes : unit -> int option
 val set_margin : int option -> unit
 val get_margin : unit -> int option
 
-(** Headers for tagging *)
-val err_hdr : Pp.std_ppcmds
-val ann_hdr : Pp.std_ppcmds
-
 (** 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
 
+(** Color output *)
 val init_color_output : unit -> unit
 val clear_styles : unit -> unit
 val parse_color_config : string -> unit
 val dump_tags : unit -> (string * Terminal.style) list
 
+(** Error printing *)
+(* To be deprecated when we can fully move to feedback-based error
+   printing. *)
+val pr_loc : Loc.t -> Pp.std_ppcmds
+val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit
+
 (** [with_output_to_file file f x] executes [f x] with logging
     redirected to a file [file] *)
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b