]> matita.cs.unibo.it Git - helm.git/blobdiff - components/getter/http_getter.ml
new compose tactic, still undocumented.
[helm.git] / components / getter / http_getter.ml
index 1b47a6c38ad6f5490acbcd455270492187325ea0..3f5cb2e5cf770d6026e32cd458ffaa2062a2cd29 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,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