]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/urimanager/uriManager.ml
moved string_of_uriref from MQueryMisc to UriManager
[helm.git] / helm / ocaml / urimanager / uriManager.ml
index 39d058b5e54c0f749a7606150f6ddfc004eb7d73..3028cf2b9b37e5d527bf35e6d89a07ed23ea7f72 100644 (file)
@@ -138,3 +138,14 @@ let innertypesuri_of_uri uri =
    newuri.(Array.length cicuri - 2) <- (string_of_uri cicuri) ^ ".types" ;
    newuri
 ;;
+
+type uriref = uri * (int list)
+
+let string_of_uriref (uri, fi) =
+   let str = string_of_uri uri in
+   let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
+   match fi with
+      | []          -> str 
+      | [t]         -> str ^ xp t ^ ")" 
+      | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" 
+