[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

10 files changed, 81 insertions, 118 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 9f33756df..66feae761 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -116,25 +116,6 @@ let strbrk s =
     else if p = n then [] else [str (String.sub s p (n-p))]
   in Ppcmd_glue (aux 0 0)
 
-let pr_loc_pos loc =
-  if Loc.is_ghost loc then (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    int (fst loc) ++ str"-" ++ int (snd loc)
-
-let pr_loc loc =
-  if Loc.is_ghost loc then str"<unknown>" ++ fnl ()
-  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":" ++ fnl ())
-    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":" ++ fnl())
-
 let ismt = function | Ppcmd_empty -> true | _ -> false
 
 (* boxing commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 802ffe8e7..7a191b01a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -171,7 +171,6 @@ val surround : std_ppcmds -> std_ppcmds
 (** Surround with parenthesis. *)
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-val pr_loc : Loc.t -> std_ppcmds
 
 (** {6 Main renderers, to formatter and to string } *)
 
diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out
index 851ecd930..776dfeb55 100644
--- a/test-suite/output/ErrorInModule.out
+++ b/test-suite/output/ErrorInModule.out
@@ -1,2 +1,3 @@
 File "stdin", line 3, characters 20-31:
 Error: The reference nonexistent was not found in the current environment.
+
diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out
index 851ecd930..776dfeb55 100644
--- a/test-suite/output/ErrorInSection.out
+++ b/test-suite/output/ErrorInSection.out
@@ -1,2 +1,3 @@
 File "stdin", line 3, characters 20-31:
 Error: The reference nonexistent was not found in the current environment.
+
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
index 9300c3f54..e9c70d1ef 100644
--- a/test-suite/output/qualification.out
+++ b/test-suite/output/qualification.out
@@ -1,3 +1,4 @@
 File "stdin", line 19, characters 0-7:
 Error: Signature components for label test do not match: expected type
 "Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
+
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index bbe4fb84c..8e6f9ffb5 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -52,7 +52,6 @@ let resynch_buffer ibuf =
    to avoid interfering with utf8. Compatibility code removed. *)
 
 let emacs_prompt_startstring() = Printer.emacs_str "<prompt>"
-
 let emacs_prompt_endstring() = Printer.emacs_str "</prompt>"
 
 (* Read a char in an input channel, displaying a prompt at every
@@ -83,6 +82,7 @@ let reset_input_buffer ic ibuf =
   ibuf.start <- 0
 
 (* Functions to print underlined locations from an input buffer. *)
+module TopErr = struct
 
 (* Given a location, returns the list of locations of each line. The last
    line is returned separately. It also checks the location bounds. *)
@@ -124,10 +124,11 @@ let blanch_utf8_string s bp ep = let open Bytes in
   done;
   Bytes.sub_string s' 0 !j
 
+let adjust_loc_buf ib loc = let open Loc in
+  { loc with ep = loc.ep - ib.start; bp = loc.bp - ib.start }
+
 let print_highlight_location ib loc =
   let (bp,ep) = Loc.unloc loc in
-  let bp = bp - ib.start
-  and ep = ep - ib.start in
   let highlight_lines =
     match get_bols_of_loc ib (bp,ep) with
       | ([],(bl,el)) ->
@@ -147,28 +148,58 @@ let print_highlight_location ib loc =
                       str sn ++ str dn) in
 	  (l1 ++ li ++ ln)
   in
-  let loc  = Loc.make_loc (bp,ep) in
-  (Pp.pr_loc loc ++ highlight_lines ++ fnl ())
-
-(* Functions to report located errors in a file. *)
-
-let print_location_in_file loc =
-  let fname = loc.Loc.fname in
-  let errstrm = str"Error while reading " ++ str fname in
-  if Loc.is_ghost loc then
-    hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
-  else
-    let errstrm = mt ()
-      (* if String.equal outer_fname fname then mt() else errstrm ++ str":" ++ fnl() *)
-    in
-    let open Loc in
-    hov 0 (* No line break so as to follow emacs error message format *)
-	(errstrm ++ Pp.pr_loc loc)
+  highlight_lines
 
 let valid_buffer_loc ib loc =
   not (Loc.is_ghost loc) &&
   let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
 
+(* 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":")
+
+(* Toplevel error explanation. *)
+let error_info_for_buffer ?loc buf =
+  Option.map (fun loc ->
+      let fname = loc.Loc.fname in
+      let hl, loc =
+        (* We are in the toplevel *)
+        if String.equal fname "" then
+          let nloc = adjust_loc_buf buf loc in
+          if valid_buffer_loc buf loc then
+            (fnl () ++ print_highlight_location buf nloc, nloc)
+            (* in the toplevel, but not a valid buffer *)
+          else (mt (), nloc)
+          (* we are in batch mode, don't adjust location *)
+        else (mt (), loc)
+      in pr_loc loc ++ hl
+    ) loc
+
+(* Actual printing routine *)
+let print_error_for_buffer ?loc lvl msg buf =
+  let pre_hdr = error_info_for_buffer ?loc buf in
+  if !Flags.print_emacs
+  then Topfmt.emacs_logger ?pre_hdr lvl msg
+  else Topfmt.std_logger   ?pre_hdr lvl msg
+
+let print_toplevel_parse_error (e, info) buf =
+  let loc = Loc.get_loc info in
+  let lvl = Feedback.Error in
+  let msg = CErrors.iprint (e, info) in
+  print_error_for_buffer ?loc lvl msg buf
+
+end
+
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
     otherwise. We trap all exceptions to prevent the error message printing
     from cycling. *)
@@ -178,18 +209,6 @@ let make_prompt () =
   with Proof_global.NoCurrentProof ->
     "Coq < "
 
-(*let build_pending_list l =
-  let pl = ref ">" in
-  let l' = ref l in
-  let res =
-    while List.length !l' > 1 do
-      pl := !pl ^ "|" Names.Id.to_string x;
-      l':=List.tl !l'
-    done in
-  let last = try List.hd !l' with _ ->   in
-  "<"^l'
-*)
-
 (* the coq prompt added to the default one when in emacs mode
    The prompt contains the current state label [n] (for global
    backtracking) and the current proof state [p] (for proof
@@ -234,29 +253,6 @@ let set_prompt prompt =
     ^ prompt ()
     ^ emacs_prompt_endstring())
 
-(* The following exceptions need not be located. *)
-
-let locate_exn = function
-  | Out_of_memory | Stack_overflow | Sys.Break -> false
-  | _ -> true
-
-(* Toplevel error explanation. *)
-
-let print_toplevel_error (e, info) =
-  let loc = Option.default Loc.ghost (Loc.get_loc info) in
-  let fname = loc.Loc.fname in
-  let locmsg =
-    if Loc.is_ghost loc || String.equal fname "" then
-      if locate_exn e && valid_buffer_loc top_buffer loc then
-	print_highlight_location top_buffer loc
-      else mt ()
-    else print_location_in_file loc
-  in
-  let hdr_text =
-    if CErrors.is_anomaly e then Topfmt.ann_hdr else Topfmt.err_hdr in
-  let hdr msg = hov 0 (hdr_text ++ msg) in
-  locmsg ++ hdr (CErrors.iprint (e, info))
-
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =
   let rec dot st = match Compat.get_tok (Stream.next st) with
@@ -285,6 +281,7 @@ let read_sentence input =
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
+    TopErr.print_toplevel_parse_error reraise top_buffer;
     iraise reraise
 
 (** Coqloop Console feedback handler *)
@@ -302,17 +299,8 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   | FileDependency (_,_) -> ()
   | FileLoaded (_,_) -> ()
   | Custom (_,_,_) -> ()
-  | Message (Error,loc,msg) ->
-    (* We ignore errors here as we (still) have a different error
-       printer for the toplevel. It is hard to solve due the many
-       error paths presents, and the different compromise of feedback
-       error forwaring in the stm depending on the mode *)
-    ()
   | Message (lvl,loc,msg) ->
-    if !Flags.print_emacs then
-      Topfmt.emacs_logger ?loc lvl msg
-    else
-      Topfmt.std_logger ?loc lvl msg
+    TopErr.print_error_for_buffer ?loc lvl msg top_buffer
 
 (** [do_vernac] reads and executes a toplevel phrase, and print error
     messages when an exception is raised, except for the following:
@@ -336,13 +324,13 @@ let do_vernac () =
         top_stderr (fnl ()); raise CErrors.Quit
     | CErrors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise CErrors.Drop
-        else top_stderr (str "There is no ML toplevel.")
-    | any ->
-        (** Main error printer, note that this didn't it the "emacs"
-            legacy path. *)
-        let any = CErrors.push any in
-        let msg = print_toplevel_error any ++ fnl () in
-        top_stderr msg
+        else Feedback.msg_error (str "There is no ML toplevel.")
+    (* Exception printing is done now by the feedback listener. *)
+    (* XXX: We need this hack due to the side effects of the exception
+       printer and the reliance of Stm.define on attaching crutial
+       state to exceptions *)
+    | any -> ignore (CErrors.(iprint (push any)))
+
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -369,7 +357,7 @@ let rec loop () =
     | CErrors.Drop -> ()
     | CErrors.Quit -> exit 0
     | any ->
-      top_stderr (str"Anomaly: main loop exited with exception: " ++
+      Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++
                   str (Printexc.to_string any) ++
                   fnl() ++
                   str"Please report" ++
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index eb61084e0..8a34ded6d 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -26,12 +26,7 @@ type input_buffer = {
 val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
-(** Toplevel error explanation, dealing with locations, Drop, Ctrl-D
-  May raise only the following exceptions: [Drop] and [End_of_input],
-  meaning we get out of the Coq loop. *)
-
-val print_toplevel_error : Exninfo.iexn -> std_ppcmds
-
+(** Toplevel feedback printer. *)
 val coqloop_feed : Feedback.feedback -> unit
 
 (** Parse and execute one vernac command. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0cd5498fe..4968804fd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -653,10 +653,10 @@ let init_toplevel arglist =
       flush_all();
       let msg =
         if !batch_mode then mt ()
-        else str "Error during initialization:" ++ fnl ()
+        else str "Error during initialization: " ++ CErrors.iprint any ++ fnl ()
       in
       let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in
-      fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any))
+      fatal_error msg (is_anomaly (fst any))
   end;
   if !batch_mode then begin
     flush_all();
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