From cfff4940f12cd8f82c745e84403317b9eee964e7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 1 Feb 2005 17:54:49 +0000 Subject: [PATCH] added strip_xpointer: remove trailing #xpointer from a UriManager.uri value --- helm/ocaml/urimanager/uriManager.ml | 7 +++++++ helm/ocaml/urimanager/uriManager.mli | 2 ++ 2 files changed, 9 insertions(+) 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 -- 2.39.2