diff options
author | 2017-04-19 10:41:40 +0200 | |
---|---|---|
committer | 2017-04-19 10:41:40 +0200 | |
commit | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (patch) | |
tree | 4a58470178b2f18952473db9ccfee393aa8b3af9 | |
parent | e5ee848ac9180b7074b97f87c4ba057241f2979e (diff) | |
parent | 12d6d60dc10654b60a31dc5bdca765409dd4898f (diff) |
Merge PR#573: [toplevel] Fix printing of parsing errors + corner case.
-rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
-rw-r--r-- | toplevel/vernac.ml | 12 |
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); |