diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-11-26 10:58:57 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-11-27 15:12:06 +0100 |
| commit | c48d806ab20951916ed5a7062eabef440f314fbe (patch) | |
| tree | 6ed1176d283ade59236cbb95a0eea5072b50b32e /ide/coqOps.ml | |
| parent | 29041ea835cb568b4343aa3ed4e2d1ee9be46f60 (diff) | |
CoqIDE: show error message for parsing errors
Diffstat (limited to 'ide/coqOps.ml')
| -rw-r--r-- | ide/coqOps.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 57f6b04d4..8b8f0791d 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; |