X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualLexer2.ml;h=7606344d1b1feea9981fd442e1228084f48ff7b1;hb=2e82e55532af778653ad53b563e4dc97cda20798;hp=92a24ec8278b2d50dcb26598b3e81f4d17878160;hpb=249d79bebff886846fbab65cc079623d90684baf;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 92a24ec82..7606344d1 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -53,13 +53,15 @@ 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 uri_step = (alpha (ident_cont|'-')*)
 let regexp meta = implicit num
 let regexp qstring = '"' [^ '"']* '"'
+let regexp uri_suffix = "con"|"ind"|"var"
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
-  ident ('/' ident)*                  (* path *)
-  ('.' ident)+                        (* ext *)
-  ("#xpointer(" num ('/' num)+ ")")?    (* xpointer *)
+  uri_step ('/' uri_step)*            (* path *)
+  ('.' uri_suffix)+                   (* ext *)
+  ("#xpointer(" num ('/' num)+ ")")?  (* xpointer *)
 (* let regexp catchall = .* *)
 
 let keywords = Hashtbl.create 17