diff options
Diffstat (limited to 'ide/coq_lex.mll')
| -rw-r--r-- | ide/coq_lex.mll | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index b6286c49..1fdd7317 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) { @@ -17,7 +19,13 @@ let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) -let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+ +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) @@ -65,7 +73,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; |