[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.

3 files changed, 56 insertions, 52 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.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f5f43ff66..9cf075065 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -430,10 +430,10 @@ let get_native_name s =
 
 (** Prints info which is either an error or an anomaly and then exits
     with the appropriate error code *)
-let fatal_error info anomaly =
-  let msg = info ++ fnl () in
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
-  exit (if anomaly then 129 else 1)
+let fatal_error ?extra exn =
+  Topfmt.print_err_exn ?extra exn;
+  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
+  exit exit_code
 
 let parse_args arglist =
   let args = ref arglist in
@@ -596,11 +596,7 @@ let parse_args arglist =
   in
   try
     parse ()
-  with
-    | UserError(_, s) as e ->
-      if ismt s then exit 1
-      else fatal_error (CErrors.print e) false
-    | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any)
+  with any -> fatal_error any
 
 let init_toplevel arglist =
   init_gc ();
@@ -646,14 +642,13 @@ let init_toplevel arglist =
       check_vio_tasks ();
       outputstate ()
     with any ->
-      let any = CErrors.push any in
       flush_all();
-      let msg =
-        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then mt ()
-        else str "Error during initialization: " ++ CErrors.iprint any ++ fnl ()
+      let extra =
+        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+        then None
+        else Some (str "Error during initialization: ")
       in
-      let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in
-      fatal_error msg (is_anomaly (fst any))
+      fatal_error ?extra any
   end;
   if !batch_mode then begin
     flush_all();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f81f77e6e..8bcf2114b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -107,6 +107,16 @@ let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
   with Proof_global.NoCurrentProof -> Pp.str ""
 
+let vernac_error msg =
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg;
+  flush_all ();
+  exit 1
+
+(* Reenable when we get back to feedback printing *)
+(* let is_end_of_input any = match any with *)
+(*     Stm.End_of_input -> true *)
+(*   | _ -> false *)
+
 let rec interp_vernac sid po (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
@@ -161,17 +171,25 @@ and load_vernac verbosely sid file =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc, ast =
+          Stm.parse_sentence !rsid in_pa
+        (* If an error in parsing occurs, we propagate the exception
+           so the caller of load_vernac will take care of it. However,
+           in the future it could be possible that we want to handle
+           all the errors as feedback events, thus in this case we
+           should relay the exception here for convenience. A
+           possibility is shown below, however we may want to refactor
+           this code:
+
         try Stm.parse_sentence !rsid in_pa
         with
-        | Stm.End_of_input -> raise Stm.End_of_input
-        | any ->
+        | any when not is_end_of_input any ->
           let (e, info) = CErrors.push any in
           let loc = Loc.get_loc info in
           let msg = CErrors.iprint (e, info) in
           Feedback.msg_error ?loc msg;
           iraise (e, info)
+       *)
       in
-
       (* Printing of vernacs *)
       if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast);
       Option.iter (vernac_echo loc) in_echo;
@@ -231,13 +249,10 @@ let chop_extension f =
 let ensure_bname src tgt =
   let src, tgt = Filename.basename src, Filename.basename tgt in
   let src, tgt = chop_extension src, chop_extension tgt in
-  if src <> tgt then begin
-    Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
-                        str "Source: " ++ str src                                                ++ fnl () ++
-                        str "Target: " ++ str tgt);
-    flush_all ();
-    exit 1
-  end
+  if src <> tgt then
+    vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
+                  str "Source: " ++ str src                                                ++ fnl () ++
+                  str "Target: " ++ str tgt)
 
 let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
 
@@ -246,17 +261,15 @@ let ensure_vo v vo = ensure ".vo" v vo
 let ensure_vio v vio = ensure ".vio" v vio
 
 let ensure_exists f =
-  if not (Sys.file_exists f) then begin
-    Feedback.msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f));
-    exit 1
-  end
+  if not (Sys.file_exists f) then
+    vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
-    if not (List.is_empty pfs) then
-      (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+    if not (List.is_empty pfs) then vernac_error (str "There are pending proofs")
+  in
   match !Flags.compilation_mode with
   | BuildVo ->
       let long_f_dot_v = ensure_v f in
@@ -311,5 +324,8 @@ let compile verbosely f =
 
 let compile v f =
   ignore(CoqworkmgrApi.get 1);
-  compile v f;
+  begin
+    try compile v f
+    with any -> Topfmt.print_err_exn any
+  end;
   CoqworkmgrApi.giveback 1