Bug fixed: uris can contain '-' (e.g. cic:/Sophia-Antipolis/...)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 92a24ec8278b2d50dcb26598b3e81f4d17878160..7606344d1b1feea9981fd442e1228084f48ff7b1 100644 (file)
--- 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

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 7b0360b9cef2c7f4b4410ddbe568defb3ed167a3..9a4340f9fb4b692a9c797e63de88875f57c5ff6f 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -585,12 +585,9 @@ EXTEND
       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
       let rex = Str.regexp ("^"^ident^"$") in
       if Str.string_match rex id 0 then
-        let rex = Str.regexp 
-          ("^\\(cic:/\\|theory:/\\)"^ident^
-           "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^
-           "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$") 
-        in
-        if Str.string_match rex uri 0 then
+        if (try ignore (UriManager.uri_of_string uri); true
+            with UriManager.IllFormedUri _ -> false)
+        then
           TacticAst.Ident_alias (id, uri)
         else 
           raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri))