diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-15 14:27:04 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-15 14:27:04 +0000 |
| commit | 9cd887e95a320d22c8158888a996fa6e50fd1189 (patch) | |
| tree | 66ea31d73432f603bace00b683fff068c155b536 | |
| parent | 32e3ed47b676960383d53961492374526189161d (diff) | |
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
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/find_phrase.mll | 12 |
2 files changed, 10 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index bfbee58ca..11af7ada6 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 965ba206f..1e608bf75 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 |