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