From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 1 Feb 2005 17:54:49 +0000 (+0000)
Subject: added strip_xpointer: remove trailing #xpointer from a UriManager.uri value
X-Git-Tag: V_0_1_0~70
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cfff4940f12cd8f82c745e84403317b9eee964e7;p=helm.git

added strip_xpointer: remove trailing #xpointer from a UriManager.uri value
---

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index cd7f9a119..00cf4faa7 100644
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -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 = 
diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli
index 703b0b4f1..12775af8d 100644
--- a/helm/ocaml/urimanager/uriManager.mli
+++ b/helm/ocaml/urimanager/uriManager.mli
@@ -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