X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Furimanager%2FuriManager.ml;h=eb0388cc297a80e0e6a29f7f5fe3ef31af864102;hb=cac9adb1a32e6bf27148ef6138aebbde500861ba;hp=9ff6a796656cbcc4995ece2d97007101ff965d4c;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/urimanager/uriManager.ml b/components/urimanager/uriManager.ml index 9ff6a7966..eb0388cc2 100644 --- a/components/urimanager/uriManager.ml +++ b/components/urimanager/uriManager.ml @@ -55,6 +55,13 @@ let name_of_uri (uri, _) = let index1 = String.rindex_from uri xpointer_offset '/' + 1 in let index2 = String.rindex uri '.' in String.sub uri index1 (index2 - index1) + +let nameext_of_uri (uri, _) = + let xpointer_offset, mah = + try String.rindex uri '#', 0 with Not_found -> String.length uri - 1, 1 + in + let index1 = String.rindex_from uri xpointer_offset '/' + 1 in + String.sub uri index1 (xpointer_offset - index1 + mah) let buri_of_uri (uri,_) = let xpointer_offset =