diff options
author | Paul Steckler <steck@stecksoft.com> | 2018-01-26 13:35:48 -0500 |
---|---|---|
committer | Paul Steckler <steck@stecksoft.com> | 2018-01-26 13:35:48 -0500 |
commit | 31956d0f0a821d904ea3d62a954ce104e6fadb4a (patch) | |
tree | b747952cefdc5abb56baba1ca203d342845c7618 /ide | |
parent | d0e05a1964fb2af093ac2a15a75bb84d342bf1ad (diff) |
allow vernacular controls before focus selector, issue #6587
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coq_lex.mll | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index a7e9003db..fcc242e07 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -19,8 +19,12 @@ let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) let number = [ '0'-'9' ]+ +let string = "\"" _+ "\"" + let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ +let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number + let dot_sep = '.' (space | eof) let utf8_extra_byte = [ '\x80' - '\xBF' ] @@ -67,7 +71,7 @@ and sentence initial stamp = parse stamp (utf8_lexeme_start lexbuf) Tags.Script.sentence; sentence true stamp lexbuf } - | undotted_sep { + | (vernac_control space+)* undotted_sep { (* Separators like { or } and bullets * - + are only active at the start of a sentence *) if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence; |