X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;h=a4d2604851bf11a85077be94542efc729060075a;hb=d9bd1adaa8588112818d3b6977a5c42a03755a21;hp=cd7f9a119ba38409f121604473f06400bafc4756;hpb=17b586f742e5c58501d62c81b6c517f5ba039f1d;p=helm.git

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index cd7f9a119..a4d260485 100644
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -36,6 +36,7 @@ let eq uri1 uri2 =
  uri1 == uri2
 ;;
 
+
 let string_of_uri uri =
   match  uri.(Array.length uri - 1) with
   | "" -> 
@@ -43,6 +44,8 @@ let string_of_uri uri =
   | _ -> 
       String.concat "#" 
         [ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ]
+
+
 let name_of_uri uri = uri.(Array.length uri - 2);;
 let buri_of_uri uri = uri.(Array.length uri - 4);;
 let depth_of_uri uri = Array.length uri - 3;;
@@ -117,6 +120,13 @@ let uri_of_string str =
       uri
 ;;
 
+let strip_xpointer uri =
+  let stripped_uri = Array.copy uri in
+  stripped_uri.(Array.length uri - 1) <- "";  (* reset xpointer field *)
+  let stripped_uri_str = string_of_uri stripped_uri in
+  set_of_uri := SetOfStrings.add stripped_uri_str stripped_uri !set_of_uri;
+  stripped_uri
+
 let cicuri_of_uri uri =
  let completeuri = string_of_uri uri in
   let newcompleteuri = 
@@ -172,3 +182,16 @@ let string_of_uriref (uri, fi) =
       | [t]         -> str ^ xp t ^ ")" 
       | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" 
 
+let compare u1 u2 =
+  let su1 = string_of_uri u1 in
+  let su2 = string_of_uri u2 in
+  Pervasives.compare su1 su2
+
+module OrderedUri =
+struct
+  type t = uri
+  let compare = compare (* the one above, not Pervasives.compare *)
+end
+
+module UriSet = Set.Make (OrderedUri)
+