aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq_lex.mll4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 7eb0f28c87..c8e5b939fe 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -17,7 +17,7 @@
let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *)
-let undotted_sep = [ '{' '}' '-' '+' '*' ]
+let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+
let dot_sep = '.' (space | eof)
@@ -68,7 +68,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 (utf8_lexeme_start lexbuf) Tags.Script.sentence;
+ if initial then stamp (Lexing.lexeme_end lexbuf) Tags.Script.sentence;
sentence initial stamp lexbuf
}
| space+ {