diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:08:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:24 +0200 |
| commit | 467db5040fe2f311f8f5493f89dc8f95647a9a0b (patch) | |
| tree | 5ebbe4139abc44bbef7362aa860c57711d6dcfd9 /ide/coq_lex.mll | |
| parent | 8e3c749e69649fb45750355e464ce7c16a4462c7 (diff) | |
Uncountably many bullets (+,-,*,++,--,**,+++,...).
Diffstat (limited to 'ide/coq_lex.mll')
| -rw-r--r-- | ide/coq_lex.mll | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 7eb0f28c8..c8e5b939f 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+ { |