X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgetter%2Fhttp_getter.ml;h=b41c4788f2a77edfd7119b8bb49a0d89b71be622;hb=55891f80b4f14251dfd5c9111f22f5edcbde2e11;hp=1b47a6c38ad6f5490acbcd455270492187325ea0;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/getter/http_getter.ml b/components/getter/http_getter.ml
index 1b47a6c38..b41c4788f 100644
--- a/components/getter/http_getter.ml
+++ b/components/getter/http_getter.ml
@@ -103,10 +103,11 @@ let ls_remote lsuri = not_implemented "ls_remote"
 let exists_remote uri = not_implemented "exists_remote"
   (* </TODO> *)
 
-let resolve_remote uri =
+let resolve_remote ~writable uri =
   (* deliver resolve request to http_getter *)
   let doc =
-    Http_getter_wget.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri)
+    Http_getter_wget.get (sprintf "%sresolve?uri=%s&writable=%b" (getter_url ())
+      uri writable)
   in
   let res = ref Unknown in
   let start_element tag attrs =
@@ -131,9 +132,9 @@ 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
+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
@@ -142,35 +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 resolve uri =
+let is_an_obj s = 
+  try 
+    s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
+  with UriManager.IllFormedUri _ -> true
+    
+let resolve ~local ~writable uri =
+  if remote () then
+    resolve_remote ~writable uri
+  else
+   let uri = deref_index_theory ~local uri in
+    try
+      if is_an_obj uri then
+        Http_getter_storage.resolve ~writable ~local (uri ^ xml_suffix)
+      else
+        Http_getter_storage.resolve ~writable ~local uri
+    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
+
+let filename ~local ~writable uri =
   if remote () then
-    resolve_remote uri
+    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 (uri ^ xml_suffix)
+      Http_getter_storage.resolve 
+        ~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
@@ -237,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
@@ -250,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
@@ -272,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 _ -> ());
@@ -285,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
@@ -318,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
@@ -336,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
@@ -345,8 +364,13 @@ let getalluris () =
 (* Shorthands from now on *)
 
 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 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