From 941807b52d8dda07f231bd8ecd8cb6003abb3195 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 3 Nov 2005 17:36:39 +0000 Subject: [PATCH] Bug fix: index.theory dereferentiation works also for exists and resolve. --- helm/ocaml/getter/http_getter.ml | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 53f4951c7..3fe39a406 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -129,6 +129,13 @@ let resolve_remote uri = | Exception e -> raise e | Resolved url -> url +let deref_index_theory uri = + if Http_getter_storage.exists (uri ^ xml_suffix) then uri + else if is_theory_uri uri && Filename.basename uri = "index.theory" then + strip_trailing_slash (Filename.dirname uri) ^ theory_suffix + else + uri + (* API *) let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ()) @@ -138,32 +145,24 @@ let exists uri = if remote () then exists_remote uri else + let uri = deref_index_theory uri in Http_getter_storage.exists (uri ^ xml_suffix) let resolve uri = if remote () then resolve_remote uri else + let uri = deref_index_theory uri in try Http_getter_storage.resolve (uri ^ xml_suffix) with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri) -let deref_index_theory uri = - if is_theory_uri uri && Filename.basename uri = "index.theory" then - strip_trailing_slash (Filename.dirname uri) ^ theory_suffix - else - uri - let getxml uri = if remote () then getxml_remote uri else begin let uri' = deref_index_theory uri in (try - try - Http_getter_storage.filename (uri' ^ xml_suffix) - with Http_getter_storage.Resource_not_found _ as exn -> - if uri <> uri' then Http_getter_storage.filename (uri ^ xml_suffix) - else raise (Key_not_found uri) + Http_getter_storage.filename (uri' ^ xml_suffix) with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)) end -- 2.39.2