From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 09:53:51 +0000 (+0000)
Subject: - bugfix: sequences like ".(" are now lexed, correctly, as
X-Git-Tag: V_0_0_10~53
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5cd7e02a5f443fdbd1151cd861e4723b91c8bce;p=helm.git

- 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 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     *)