]> matita.cs.unibo.it Git - helm.git/commitdiff
buri_of_uri is now #xpointer aware.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Jun 2005 09:39:28 +0000 (09:39 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Jun 2005 09:39:28 +0000 (09:39 +0000)
helm/ocaml/urimanager/uriManager.ml

index 203093c7e63e9c2644fb818bd234dfc1c6dc74fc..b8da7d91eddec50f086251bf863da6df40f99e66 100644 (file)
@@ -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 =