X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;h=9f969fdd12e11d699d53f11cb09f3029fa7bc59c;hb=08a2b1a3f1a1e9af07850089f0e0838eb052223d;hp=0fa24cfcdc8504bffff1a0be2bb8099507403e8c;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index 0fa24cfcd..9f969fdd1 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -96,7 +96,11 @@ let mk_prefixes str = in let tokens = (Str.split (Str.regexp "/") str) in (* ty = "cic:" *) - let (ty, sp) = (List.hd tokens, List.tl tokens) in + let (ty, sp) = + (try (List.hd tokens, List.tl tokens) + with Failure "hd" | Failure "tl" -> + raise (IllFormedUri str)) + in aux ty sp ;; @@ -137,3 +141,13 @@ let annuri_of_uri uri = let uri_is_annuri uri = Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0 ;; + +let bodyuri_of_uri uri = + let struri = string_of_uri uri in + if Str.string_match (Str.regexp ".*\.con$") (string_of_uri uri) 0 then + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- struri ^ ".body" ; + Some newuri + else + None +;;