]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/uriManager.mli
Initial revision
[helm.git] / helm / interface / uriManager.mli
diff --git a/helm/interface/uriManager.mli b/helm/interface/uriManager.mli
new file mode 100644 (file)
index 0000000..8cffc94
--- /dev/null
@@ -0,0 +1,15 @@
+type uri
+
+val eq : uri -> uri -> bool
+
+val uri_of_string : string -> uri
+
+val string_of_uri : uri -> string  (* complete uri *)
+val name_of_uri   : uri -> string  (* name only (without extension)*)
+val buri_of_uri   : uri -> string  (* base uri only *)
+val depth_of_uri  : uri -> int     (* length of the path *)
+
+(* relative_depth curi uri cookingsno                                        *)
+(* is the number of times to cook uri to use it when the current uri is curi *)
+(* cooked cookingsno times                                                   *)
+val relative_depth : uri -> uri -> int -> int