X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationLexer.ml;h=33fb8fd78494085a819c9d65fb11e2020a654c42;hb=49a4d6d69a54bcdfb05c893ff2208e3e045efa26;hp=3d9d6be252a3d28118d1d1f5e7af47630928d4e1;hpb=f5b76bf5f55bbd2f2053e36d4b251548f3ed8623;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 3d9d6be25..33fb8fd78 100644
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -123,9 +123,12 @@ let _ =
       ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
     ]
 
+let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ]+
+
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
-  ident ('/' ident)*                  (* path *)
+(*   ident ('/' ident)*                  |+ path +| *)
+  uri_step ('/' uri_step)*            (* path *)
   ('.' ident)+                        (* ext *)
   ("#xpointer(" number ('/' number)+ ")")?  (* xpointer *)