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

diff --git a/components/getter/http_getter.ml b/components/getter/http_getter.ml
index 1b47a6c38..3f5cb2e5c 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 =
@@ -150,13 +151,31 @@ let exists uri =
    let uri = deref_index_theory uri in
     Http_getter_storage.exists (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 ~writable uri =
+  if remote () then
+    resolve_remote ~writable uri
+  else
+   let uri = deref_index_theory uri in
+    try
+      if is_an_obj uri then
+        Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+      else
+        Http_getter_storage.resolve ~writable uri
+    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
+
+let filename ~writable uri =
   if remote () then
-    resolve_remote uri
+    raise (Key_not_found uri)
   else
    let uri = deref_index_theory uri in
     try
-      Http_getter_storage.resolve (uri ^ xml_suffix)
+      Http_getter_storage.resolve 
+        ~must_exists:false ~writable uri
     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
 
 let getxml uri =
@@ -345,8 +364,9 @@ 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 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 tilde_expand_key k =
   try