]> matita.cs.unibo.it Git - helm.git/blobdiff - components/urimanager/uriManager.ml
reverted previous fix
[helm.git] / components / urimanager / uriManager.ml
index 9ff6a796656cbcc4995ece2d97007101ff965d4c..c0da8eb4b334e5a3e01fea383fcfcc8c88879678 100644 (file)
@@ -55,6 +55,13 @@ let name_of_uri (uri, _) =
   let index1 = String.rindex_from uri xpointer_offset '/' + 1 in
   let index2 = String.rindex uri '.' in
   String.sub uri index1 (index2 - index1)
+
+let nameext_of_uri (uri, _) = 
+  let xpointer_offset, mah = 
+    try String.rindex uri '#', 0 with Not_found -> String.length uri - 1, 1
+  in
+  let index1 = String.rindex_from uri xpointer_offset '/' + 1 in
+  String.sub uri index1 (xpointer_offset - index1 + mah)
   
 let buri_of_uri (uri,_) = 
   let xpointer_offset = 
@@ -213,6 +220,19 @@ end
 
 module UriSet = Set.Make (OrderedUri)
 
+(*
+module OrderedUriPair =
+struct
+  type t = uri * uri
+  let compare (u11, u12) (u21, u22) =
+    match compare u11 u21 with
+    | 0 -> compare u12 u22
+    | x -> x
+end
+
+module UriPairSet = Set.Make (OrderedUriPair)
+*)
+
 module HashedUri =
 struct
   type t = uri