From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 21 Nov 2005 08:36:02 +0000 (+0000)
Subject: fixed URI regexp so that URIs containing '-' are allowed
X-Git-Tag: V_0_7_2_3~21
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=49a4d6d69a54bcdfb05c893ff2208e3e045efa26

fixed URI regexp so that URIs containing '-' are allowed
---

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