From 12d6d60dc10654b60a31dc5bdca765409dd4898f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 19 Apr 2017 03:13:09 +0200 Subject: [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. --- toplevel/coqtop.ml | 2 +- toplevel/vernac.ml | 12 +++++++++++- 2 files changed, 12 insertions(+), 2 deletions(-) (limited to 'toplevel') 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); -- cgit v1.2.3