[toplevel] Remove exception error printer in favor of feedback printer.

We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing
all the errors from the feedback handler, even in the case of coqtop.

All error display is handled by a single, uniform path.

There may be some minor discrepancies with 8.6 as we are uniform now
whereas 8.6 tended to print errors in several ways, but our behavior
is a subset of the 8.6 behavior.

We had to make a choice for `-emacs` error output, which used to vary
too. We have chosen to display error messages as:

```
(location info) option \n
(program caret) option \n
MARKER[254]Error: msgMARKER[255]
```

This commit also fixes:

- https://coq.inria.fr/bugs/show_bug.cgi?id=5418
- https://coq.inria.fr/bugs/show_bug.cgi?id=5429

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