diff options
| -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 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 |