From c5cd7e02a5f443fdbd1151cd861e4723b91c8bce Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 09:53:51 +0000 Subject: [PATCH] - bugfix: sequences like ".(" are now lexed, correctly, as [ SYMBOL "."; PAREN "("] instead of [ SYMBOL ".(" ] --- helm/ocaml/cic_disambiguation/cicTextualLexer2.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 2cb13cb33..8a6faa193 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -30,18 +30,20 @@ exception Not_an_extended_ident let regexp alpha = [ 'a' - 'z' 'A' - 'Z' ] let regexp digit = [ '0' - '9' ] let regexp blank = [ ' ' '\t' '\n' ] +let regexp paren = [ '(' '[' '{' ')' ']' '}' ] +let regexp implicit = '?' +let regexp symbol_char = + [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' '\\' '(' '[' '{' ')' ']' '}' ] let regexp blanks = blank+ let regexp num = digit+ let regexp tex_token = '\\' alpha+ -let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ] +let regexp symbol = symbol_char+ let regexp ident_cont = alpha | num | '_' | '\'' let regexp ident_cont' = ident_cont | tex_token let regexp ident = (alpha ident_cont*) | ('_' ident_cont+) let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+) -let regexp paren = [ '(' '[' '{' ')' ']' '}' ] -let regexp implicit = '?' -let regexp meta = '?' num +let regexp meta = implicit num let regexp qstring = '"' [^ '"']* '"' let regexp uri = (* schema *) (* path *) (* ext *) (* xpointer *) -- 2.39.2