From 9cd887e95a320d22c8158888a996fa6e50fd1189 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 15 Oct 2004 14:27:04 +0000
Subject: 2 bugs de reconnaissance de fin de phrase corriges

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6218 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml       |  2 ++
 ide/find_phrase.mll | 12 ++++++++----
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index bfbee58cad..11af7ada6b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1030,6 +1030,7 @@ object(self)
       end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
       Some (start,end_iter)
     with
+(*
     | Find_phrase.EOF s -> 
 	(* Phrase is at the end of the buffer*)
 	let si = start#offset in
@@ -1038,6 +1039,7 @@ object(self)
 	input_buffer#insert ~iter:end_iter "\n";
 	Some (input_buffer#get_iter (`OFFSET si),
 	      input_buffer#get_iter (`OFFSET ei))
+*)
     | _ -> None
 
   method complete_at_offset (offset:int) = 
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 965ba206f8..1e608bf75e 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -12,7 +12,6 @@
   exception Lex_error of string
   let length = ref 0
   let buff = Buffer.create 513
-  exception EOF of string
 
 }
 
@@ -34,10 +33,15 @@ rule next_phrase = parse
       Buffer.contents buff}
 
   | phrase_sep eof{
-      length := !length + 2; 
+      length := !length + 1; 
       Buffer.add_string buff (Lexing.lexeme lexbuf);
-      Buffer.add_char buff '\n';
-      raise (EOF(Buffer.contents buff))}
+      Buffer.contents buff}
+  | phrase_sep phrase_sep
+      { 
+	length := !length + 2; 
+	Buffer.add_string buff (Lexing.lexeme lexbuf);
+	next_phrase lexbuf
+      }
   | _ 
       { 
 	let c = Lexing.lexeme_char lexbuf 0 in 
-- 
cgit v1.2.3