]> matita.cs.unibo.it Git - helm.git/commitdiff
added strip_xpointer: remove trailing #xpointer from a UriManager.uri value
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 1 Feb 2005 17:54:49 +0000 (17:54 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 1 Feb 2005 17:54:49 +0000 (17:54 +0000)
helm/ocaml/urimanager/uriManager.ml
helm/ocaml/urimanager/uriManager.mli

index cd7f9a119ba38409f121604473f06400bafc4756..00cf4faa7a4775409eabdcb4d8610c9278a73329 100644 (file)
@@ -117,6 +117,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 = 
index 703b0b4f1629e12639d64767a2c825b274fb49c8..12775af8d48fd9a3168fbc149bfc7ebbf7ec4766 100644 (file)
@@ -40,6 +40,8 @@ val depth_of_uri  : uri -> int     (* length of the path *)
 (* i.e. removes the [.types][.ann] suffix                       *)
 val cicuri_of_uri : uri -> uri
 
+val strip_xpointer: uri -> uri      (* remove trailing #xpointer..., if any *)
+
 (* given an uri, returns the uri of the corresponding annotation file, *)
 (* i.e. adds the .ann suffix if not already present                    *)
 val annuri_of_uri : uri -> uri