X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualLexer2.ml;h=8a6faa19339fe2979b75b5407ebeca108f551ed6;hb=c5cd7e02a5f443fdbd1151cd861e4723b91c8bce;hp=2cb13cb33ade892562e006ca4292f030276e6b80;hpb=3aa4007aeb10078c7e170d8fdc681912835d2ddb;p=helm.git

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