From 2e82e55532af778653ad53b563e4dc97cda20798 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Jul 2005 15:05:10 +0000 Subject: [PATCH] Bug fixed: uris can contain '-' (e.g. cic:/Sophia-Antipolis/...) --- helm/ocaml/cic_disambiguation/cicTextualLexer2.ml | 8 +++++--- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 9 +++------ 2 files changed, 8 insertions(+), 9 deletions(-) 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 diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 7b0360b9c..9a4340f9f 100644 --- 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)) -- 2.39.2