[toplevel] Use exception information for error printing.

This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.

However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479

Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.

This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.

1 files changed, 13 insertions, 20 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4641a2bc8..b608488c8 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -149,20 +149,6 @@ 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 ->
@@ -177,7 +163,7 @@ let error_info_for_buffer ?loc buf =
           else (mt (), nloc)
           (* we are in batch mode, don't adjust location *)
         else (mt (), loc)
-      in pr_loc loc ++ hl
+      in Topfmt.pr_loc loc ++ hl
     ) loc
 
 (* Actual printing routine *)
@@ -292,6 +278,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   | FileDependency (_,_) -> ()
   | FileLoaded (_,_) -> ()
   | Custom (_,_,_) -> ()
+  (* Re-enable when we switch back to feedback-based error printing *)
+  | Message (Error,loc,msg) -> ()
+  (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *)
   | Message (lvl,loc,msg) ->
     TopErr.print_error_for_buffer ?loc lvl msg top_buffer
 
@@ -318,11 +307,15 @@ let do_vernac sid =
     | CErrors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise CErrors.Drop
         else (Feedback.msg_error (str "There is no ML toplevel."); sid)
-    (* 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))); sid
+    (* Exception printing should be done by the feedback listener,
+       however this is not yet ready so we rely on the exception for
+       now. *)
+    | any ->
+      let (e, info) = CErrors.push any in
+      let loc = Loc.get_loc info in
+      let msg = CErrors.iprint (e, info) in
+      TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+      sid
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.