From 31956d0f0a821d904ea3d62a954ce104e6fadb4a Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
Date: Fri, 26 Jan 2018 13:35:48 -0500
Subject: allow vernacular controls before focus selector, issue #6587

---
 ide/coq_lex.mll | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'ide')

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;
-- 
cgit v1.2.3