diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-10 15:47:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-10 15:47:43 +0200 |
| commit | e3798c52c3bd52d43fa84feedd7caaa4def57db8 (patch) | |
| tree | 52383fbd40b0a2251de13b6e9f78d7631f502360 /toplevel | |
| parent | dad84398ccd76f57050cf08736104fbd36c1ffee (diff) | |
Fixing #5133 (error reporting delayed).
I wrongly moved call to the function interpreting commands within a
different try-with block in 8a8caba36e.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index bdcfa8336..71e1f9593 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -274,12 +274,10 @@ let rec discard_to_dot () = | End_of_input -> raise End_of_input | e when CErrors.noncritical e -> () -let read_eval_sentence () = +let read_sentence input = try - let input = (top_buffer.tokens, None) in let (loc, _ as r) = Vernac.parse_sentence input in - CWarnings.set_current_loc loc; - Vernac.eval_expr input r + CWarnings.set_current_loc loc; r with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -300,7 +298,8 @@ let do_vernac () = if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try - read_eval_sentence () + let input = (top_buffer.tokens, None) in + Vernac.eval_expr input (read_sentence input) with | End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit |