From e3798c52c3bd52d43fa84feedd7caaa4def57db8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Oct 2016 15:47:43 +0200
Subject: Fixing #5133 (error reporting delayed).

I wrongly moved call to the function interpreting commands within a
different try-with block in 8a8caba36e.
---
 toplevel/coqloop.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index bdcfa8336d..71e1f9593d 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
-- 
cgit v1.2.3