From c48d806ab20951916ed5a7062eabef440f314fbe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Nov 2013 10:58:57 +0100 Subject: CoqIDE: show error message for parsing errors --- ide/coqOps.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 57f6b04d46..8b8f0791d9 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -402,7 +402,7 @@ object(self) buffer#remove_tag Tags.Script.to_process ~start ~stop; self#discard_command_queue queue; pop_info (); - if Stateid.equal id tip then begin + if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin self#position_error_tag_at_iter start phrase loc; buffer#place_cursor ~where:stop; messages#clear; -- cgit v1.2.3