From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 6 Jul 2005 17:20:25 +0000 (+0000)
Subject: - bugfix: correctly handle real "index.theory"
X-Git-Tag: V_0_7_1~40
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de52688df43376ca0293a5996c35d54e6832e4de;p=helm.git

- bugfix: correctly handle real "index.theory"
- removed some debugging prints
---

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 43c4be473..7695159ee 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -134,7 +134,7 @@ let resolve_remote uri =
 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
@@ -157,10 +157,14 @@ let deref_index_theory 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
+      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 exn
+    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
   end
 
 let getxslt uri =
@@ -230,18 +234,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 +285,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