From 63f9f933c4e370311cdf5da4cd9c91311404b66d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 22 Feb 2012 13:54:52 +0000
Subject: Ide: sentences found by find_phrase_starting_at should be nonempty
 (fix #2683)

 In addition to #2683, this also prevent Vernac.End_of_input
 exceptions when a buffer ends with one of the new delimiters -+*{}.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14989 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2f53fa8ff3..111a8ffc25 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -893,7 +893,9 @@ object(self)
     try
       let start = grab_sentence_start start self#get_start_of_input in
       let stop = grab_sentence_stop start in
-      if is_sentence_end stop#backward_char then Some (start,stop)
+      (* Is this phrase non-empty and complete ? *)
+      if stop#compare start > 0 && is_sentence_end stop#backward_char
+      then Some (start,stop)
       else None
     with Not_found -> None
 
-- 
cgit v1.2.3