]> matita.cs.unibo.it Git - helm.git/blobdiff - components/getter/http_getter.mli
Huge commit for the release. Includes:
[helm.git] / components / getter / http_getter.mli
index 4bbc447bdac85cca2102b21b302a05b014ac8d0a..845a17a1035b760e028aeade14bad0b36e387beb 100644 (file)
@@ -40,7 +40,11 @@ val help: unit -> string
 
   (** @raise Http_getter_types.Unresolvable_URI _
   * @raise Http_getter_types.Key_not_found _ *)
-val resolve: string -> string (* uri -> url *)
+val resolve: writable:bool -> string -> string (* uri -> url *)
+
+  (** as resolve, but does not check if the resource exists
+   * @raise Http_getter_types.Key_not_found *)
+val filename: writable:bool -> string -> string (* uri -> url *)
 
 val exists: string -> bool
 
@@ -57,8 +61,9 @@ val ls: string -> ls_item list
   (** {2 UriManager shorthands} *)
 
 val getxml'     : UriManager.uri -> string
-val resolve'    : UriManager.uri -> string
+val resolve'    : writable:bool -> UriManager.uri -> string
 val exists'     : UriManager.uri -> bool
+val filename'     : writable:bool -> UriManager.uri -> string
 
   (** {2 Misc} *)