Merge PR #6652: Allow vernacular controls before focus selector

1 files changed, 5 insertions, 1 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index a7e9003dbe..fcc242e074 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;