maxipatch for support of multiple DBs.

[helm.git] / components / getter / http_getter.ml

diff --git a/components/getter/http_getter.ml b/components/getter/http_getter.ml
index 3f5cb2e5cf770d6026e32cd458ffaa2062a2cd29..b41c4788f2a77edfd7119b8bb49a0d89b71be622 100644 (file)
--- a/components/getter/http_getter.ml
+++ b/components/getter/http_getter.ml
@@ -132,9 +132,9 @@ let resolve_remote ~writable 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
+let deref_index_theory ~local uri =
+(*  if Http_getter_storage.exists ~local (uri ^ xml_suffix) then uri *)
+ if is_theory_uri uri && Filename.basename uri = "index.theory" then
     strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
  else
     uri
@@ -143,53 +143,53 @@ let deref_index_theory uri =
 
 let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
 
-let exists uri =
+let exists ~local 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 uri = deref_index_theory ~local uri in
+    Http_getter_storage.exists ~local (uri ^ xml_suffix)
        
 let is_an_obj s = 
   try 
     s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
   with UriManager.IllFormedUri _ -> true
     
-let resolve ~writable uri =
+let resolve ~local ~writable uri =
   if remote () then
     resolve_remote ~writable uri
   else
-   let uri = deref_index_theory uri in
+   let uri = deref_index_theory ~local uri in
     try
       if is_an_obj uri then
-        Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+        Http_getter_storage.resolve ~writable ~local (uri ^ xml_suffix)
       else
-        Http_getter_storage.resolve ~writable uri
+        Http_getter_storage.resolve ~writable ~local uri
     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
 
-let filename ~writable uri =
+let filename ~local ~writable uri =
   if remote () then
     raise (Key_not_found uri)
   else
-   let uri = deref_index_theory uri in
+   let uri = deref_index_theory ~local uri in
     try
       Http_getter_storage.resolve 
-        ~must_exists:false ~writable uri
+        ~must_exists:false ~writable ~local uri
     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
 
 let getxml uri =
   if remote () then getxml_remote uri
   else begin
-    let uri' = deref_index_theory uri in
+    let uri' = deref_index_theory ~local:false uri in
     (try
-      Http_getter_storage.filename (uri' ^ xml_suffix)
+      Http_getter_storage.filename ~local:false (uri' ^ xml_suffix)
     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
   end
 
 let getxslt uri =
   if remote () then getxslt_remote uri
-  else Http_getter_storage.filename ~find:true ("xslt:/" ^ uri)
+  else Http_getter_storage.filename ~local:false ~find:true ("xslt:/" ^ uri)
 
 let getdtd uri =
   if remote () then
@@ -256,7 +256,7 @@ let collect_ls_items dirs_set objs_tbl =
 let contains_object = (<>) []
 
   (** non regexp-aware version of ls *)
-let rec dumb_ls uri_prefix =
+let rec dumb_ls ~local 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
@@ -269,7 +269,7 @@ let rec dumb_ls uri_prefix =
           try
             store_obj objs (strip_suffix ~suffix:xml_suffix fname)
           with Invalid_argument _ -> ())
-      (Http_getter_storage.ls uri_prefix);
+      (Http_getter_storage.ls ~local uri_prefix);
     collect_ls_items !dirs objs
   end else if is_theory_uri uri_prefix then begin
     let items = ref [] in
@@ -291,12 +291,12 @@ let rec dumb_ls uri_prefix =
             let fname = strip_suffix ~suffix:xml_suffix fname in
             let theory_name = strip_suffix ~suffix:theory_suffix fname in
             let sub_theory = normalize_dir cic_uri_prefix ^ theory_name ^ "/" in
-            if is_empty_theory sub_theory then add_theory fname
+            if is_empty_theory ~local sub_theory then add_theory fname
           with Invalid_argument _ -> ())
-      (Http_getter_storage.ls uri_prefix);
+      (Http_getter_storage.ls ~local uri_prefix);
     (try
-      if contains_object (dumb_ls cic_uri_prefix)
-        && exists (strip_trailing_slash uri_prefix ^ theory_suffix)
+      if contains_object (dumb_ls ~local cic_uri_prefix)
+        && exists ~local:false (strip_trailing_slash uri_prefix ^ theory_suffix)
       then
         add_theory "index.theory";
     with Unresolvable_URI _ -> ());
@@ -304,9 +304,9 @@ let rec dumb_ls uri_prefix =
   end else
     raise (Invalid_URI uri_prefix)
 
-and is_empty_theory uri_prefix =
+and is_empty_theory ~local uri_prefix =
 (*   prerr_endline ("is_empty_theory " ^ uri_prefix); *)
-  not (contains_object (dumb_ls uri_prefix))
+  not (contains_object (dumb_ls ~local uri_prefix))
 
   (* handle simple regular expressions of the form "...(..|..|..)..." on cic
    * uris, not meant to be a real implementation of regexp. The only we use is
@@ -337,12 +337,12 @@ let merge_results results =
   in
   aux [] [] (List.concat results)
 
-let ls regexp =
+let ls ~local regexp =
   if remote () then
     ls_remote regexp
   else
     let prefixes = explode_ls_regexp regexp in
-    merge_results (List.map dumb_ls prefixes)
+    merge_results (List.map (dumb_ls ~local) prefixes)
 
 let getalluris () =
   let rec aux acc = function
@@ -355,7 +355,7 @@ let getalluris () =
               | Ls_object obj -> (dir ^ obj.uri) :: acc, subdirs
               | Ls_section sect -> acc, (dir ^ sect ^ "/") :: subdirs)
             (acc, todo)
-            (dumb_ls dir)
+            (dumb_ls ~local:false dir)
         in
         aux acc' todo'
   in
@@ -364,9 +364,13 @@ let getalluris () =
 (* Shorthands from now on *)
 
 let getxml' uri = getxml (UriManager.string_of_uri uri)
-let resolve' ~writable uri = resolve ~writable (UriManager.string_of_uri uri)
-let exists' uri = exists (UriManager.string_of_uri uri)
-let filename' ~writable uri = filename  ~writable (UriManager.string_of_uri uri)
+let resolve' ~local ~writable uri =
+  resolve ~local ~writable (UriManager.string_of_uri uri)
+;;
+let exists' ~local uri = exists ~local (UriManager.string_of_uri uri)
+let filename' ~local ~writable uri =
+  filename ~local ~writable (UriManager.string_of_uri uri)
+;;
 
 let tilde_expand_key k =
   try