- bugfix: sequences like ".(" are now lexed, correctly, as

  [ SYMBOL "."; PAREN "("] instead of [ SYMBOL ".(" ]

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 2cb13cb33ade892562e006ca4292f030276e6b80..8a6faa19339fe2979b75b5407ebeca108f551ed6 100644 (file)
--- 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     *)