From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 30 Jun 2005 09:39:28 +0000 (+0000)
Subject: buri_of_uri is now #xpointer aware.
X-Git-Tag: PRE_GETTER_STORAGE~102
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c63e8332bdded20ff61d47bd5951a80c29b41942;p=helm.git

buri_of_uri is now #xpointer aware.
---

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 203093c7e..b8da7d91e 100644
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -55,7 +55,10 @@ let name_of_uri (uri, _) =
   String.sub uri index1 (index2 - index1)
   
 let buri_of_uri (uri,_) = 
-  let index = String.rindex uri '/' in
+  let xpointer_offset = 
+    try String.rindex uri '#' with Not_found -> String.length uri - 1
+  in
+  let index = String.rindex_from uri xpointer_offset '/' in
   String.sub uri 0 index
 
 module OrderedStrings =