]> matita.cs.unibo.it Git - helm.git/blobdiff - components/getter/http_getter.ml
Huge commit for the release. Includes:
[helm.git] / components / getter / http_getter.ml
index 1b47a6c38ad6f5490acbcd455270492187325ea0..d2993575a439f3770ffb35c4caab5745dd3c5dea 100644 (file)
@@ -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,23 @@ let exists uri =
    let uri = deref_index_theory uri in
     Http_getter_storage.exists (uri ^ xml_suffix)
        
-let resolve uri =
+let resolve ~writable uri =
   if remote () then
-    resolve_remote uri
+    resolve_remote ~writable uri
   else
    let uri = deref_index_theory uri in
     try
-      Http_getter_storage.resolve (uri ^ xml_suffix)
+      Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
+
+let filename ~writable uri =
+  if remote () then
+    raise (Key_not_found uri)
+  else
+   let uri = deref_index_theory uri in
+    try
+      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 +356,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