]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/getter.mli
Merge of the V7_3_new_exportation branch.
[helm.git] / helm / ocaml / getter / getter.mli
index 6b1d2ca2945da35a39e4951e06760a524842380b..3fbec8070439fa6cb5e8e1578558e50b0823ddb7 100644 (file)
@@ -51,3 +51,12 @@ val getxml : ?format:format -> ?patchdtd:bool -> UriManager.uri -> string
 
 (* adds an (URI -> URL) entry in the map from URIs to URLs *)
 val register : UriManager.uri -> string -> unit
+
+exception Unresolved
+exception UnexpectedGetterOutput
+
+(* resolves an URI to its corresponding URL.                  *)
+(* Unresolved is raised if there is no URL for the given URI. *)
+(* UnexceptedGetterOutput is raised if the output of the real *)
+(*  getter has not the expected format.                       *)
+val resolve: UriManager.uri -> string