diff options
Diffstat (limited to 'toplevel')
| -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 18a38525d..f5f43ff66 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 fd208bd89..3359a1672 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); |