diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 22:38:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 22:38:32 +0200 |
| commit | bc7bea8fd028e12b1d3199128c788af671176af7 (patch) | |
| tree | 381b63b30be0b6ac6fc91a14ee62578d9803208f /ide | |
| parent | 467db5040fe2f311f8f5493f89dc8f95647a9a0b (diff) | |
CoqIDE: fixing parsing of bullets and brackets even at end of file.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq_lex.mll | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index c8e5b939f..8b17c29df 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -13,6 +13,7 @@ let utf8_lexeme_start lexbuf = Lexing.lexeme_start lexbuf - !utf8_adjust + + String.length (Lexing.lexeme lexbuf) - 1 } let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) @@ -33,7 +34,7 @@ rule coq_string = parse and comment = parse | "(*" { let _ = comment lexbuf in comment lexbuf } | "\"" { let () = coq_string lexbuf in comment lexbuf } - | "*)" { Some (utf8_lexeme_start lexbuf + 1) } + | "*)" { Some (utf8_lexeme_start lexbuf) } | eof { None } | utf8_extra_byte { incr utf8_adjust; comment lexbuf } | _ { comment lexbuf } @@ -68,7 +69,7 @@ and sentence initial stamp = parse | undotted_sep { (* Separators like { or } and bullets * - + are only active at the start of a sentence *) - if initial then stamp (Lexing.lexeme_end lexbuf) Tags.Script.sentence; + if initial then stamp (utf8_lexeme_start lexbuf) Tags.Script.sentence; sentence initial stamp lexbuf } | space+ { |