X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=191117a20e38c182d3af6a43824cf8c27af198af;hb=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;hp=43c4be4737259302b856b79a880d36494ad2f1f9;hpb=3969a288b2c18b1b4da9a9941a8a3a77480dd4d1;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 43c4be473..191117a20 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -129,38 +129,41 @@ 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 ())
 
 let exists uri =
-  prerr_endline ("Http_getter.exists " ^ uri);
+(*   prerr_endline ("Http_getter.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
-    try
-      let uri = deref_index_theory uri in
-      Http_getter_storage.filename (uri ^ xml_suffix)
-    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
+    let uri' = deref_index_theory uri in
+    (try
+      Http_getter_storage.filename (uri' ^ xml_suffix)
+    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
   end
 
 let getxslt uri =
@@ -230,18 +233,10 @@ let collect_ls_items dirs_set objs_tbl =
   List.rev !items
 
 let contains_object = (<>) []
-(*   List.iter
-    (function
-      | Ls_section name -> prerr_endline (name ^ "/");
-      | Ls_object obj -> prerr_endline obj.uri)
-    l;
-  prerr_endline (string_of_bool b);
-  b *)
-(*   List.exists (function Ls_object _ -> true | _ -> false) *)
 
   (** non regexp-aware version of ls *)
 let rec dumb_ls uri_prefix =
-  prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix);
+(*   prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix); *)
   if is_cic_obj_uri uri_prefix then begin
     let dirs = ref StringSet.empty in
     let objs = Hashtbl.create 17 in
@@ -289,7 +284,7 @@ let rec dumb_ls uri_prefix =
     raise (Invalid_URI uri_prefix)
 
 and is_empty_theory uri_prefix =
-  prerr_endline ("is_empty_theory " ^ uri_prefix);
+(*   prerr_endline ("is_empty_theory " ^ uri_prefix); *)
   not (contains_object (dumb_ls uri_prefix))
 
   (* handle simple regular expressions of the form "...(..|..|..)..." on cic
@@ -351,7 +346,13 @@ let getxml' uri = getxml (UriManager.string_of_uri uri)
 let resolve' uri = resolve (UriManager.string_of_uri uri)
 let exists' uri = exists (UriManager.string_of_uri uri)
 
+let tilde_expand_key k =
+  try
+    Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
+  with Helm_registry.Key_not_found _ -> ()
+
 let init () =
+  List.iter tilde_expand_key ["getter.cache_dir"; "getter.dtd_dir"];
   Http_getter_logger.set_log_level
     (Helm_registry.get_opt_default Helm_registry.int ~default:1
       "getter.log_level");