From d411a796341a138cacd72350715871f48f82920b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 5 May 2017 21:31:14 +0200
Subject: [toplevel] Fix a couple of logical errors in error printing.

In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use
exceptions for error printing. However a couple of mistakes were
present in that commit:

- We wrongly absorbed the exception on `Vernac.compile`. However, it
  should be propagated as the caller will correctly print the error
  now. This introduced a critical bug as now `coqc` return the wrong
  exit status on error, breaking all sort of things.

- We printed parsing exceptions twice; now it is not necessary to
  print the exception in the parsing handler as it will be propagated.

I've checked this commit versus all previously reported bugs and it
seems to work; we should definitively add a test-suite case to check
that the exit code of `coqc` is correct, plus several other cases such
as bugs

https://coq.inria.fr/bugs/show_bug.cgi?id=5467
https://coq.inria.fr/bugs/show_bug.cgi?id=5485
https://coq.inria.fr/bugs/show_bug.cgi?id=5484

etc... See also PR #583
---
 toplevel/coqloop.ml | 8 ++++++--
 toplevel/vernac.ml  | 5 +----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 9a4f476bd3..a80599cd57 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -173,12 +173,13 @@ let print_error_for_buffer ?loc lvl msg buf =
   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"
@@ -260,7 +261,10 @@ let read_sentence sid input =
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
-    TopErr.print_toplevel_parse_error reraise top_buffer;
+    (* The caller of read_sentence does the error printing now, this
+       should be re-enabled once we rely on the feedback error
+       printer again *)
+    (* TopErr.print_toplevel_parse_error reraise top_buffer; *)
     Exninfo.iraise reraise
 
 (** Coqloop Console feedback handler *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9f6f77ef1d..4fca4ea184 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -323,8 +323,5 @@ let compile verbosely f =
 
 let compile v f =
   ignore(CoqworkmgrApi.get 1);
-  begin
-    try compile v f
-    with any -> Topfmt.print_err_exn any
-  end;
+  compile v f;
   CoqworkmgrApi.giveback 1
-- 
cgit v1.2.3