[toplevel] Fix printing of parsing errors + corner case.

PR #441 and #530 had an interesting interaction creating two bugs:

- #441 stopped emitting feedback for the parser, however #530 changed
  the mechanism to print parser errors to the feedback, thus when the
  two patches were applied, parsing errors were not printed in
  batch_mode.

- Additionally, #530 contains an error: prior to `Stm.init` we must
  take care of exceptions `require ()`/etc... otherwise they won't get
  printed.

2 files changed, 12 insertions, 2 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c259beb17..a4dcefcbd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -649,7 +649,7 @@ let init_toplevel arglist =
       let any = CErrors.push any in
       flush_all();
       let msg =
-        if !batch_mode then mt ()
+        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then mt ()
         else str "Error during initialization: " ++ CErrors.iprint any ++ fnl ()
       in
       let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 18f93197c..84330b88a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -162,7 +162,17 @@ and load_vernac verbosely sid file =
     (* we go out of the following infinite loop when a End_of_input is
      * 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 in
+      let loc, ast =
+        try Stm.parse_sentence !rsid in_pa
+        with
+        | Stm.End_of_input -> raise Stm.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);