X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;h=9ff6a796656cbcc4995ece2d97007101ff965d4c;hb=4c2a5e7da43e15d9a5f35d65f6bd6eda9a117d93;hp=f0bc5795892891ac813b14ed0d45c2e8396df871;hpb=45c8cad0524aa224f530ac3829adc8a1adfef4d5;p=helm.git diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index f0bc57958..9ff6a7966 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* * "cic:/a/b/c.con" => ("cic:/a/b/c.con", id ) * "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id) @@ -81,8 +83,10 @@ exception IllFormedUri of string;; let _dottypes = ".types" let _types = "types",5 -let _ann = "ann",3 +let _dotuniv = ".univ" +let _univ = "univ",4 let _dotann = ".ann" +let _ann = "ann",3 let _var = "var",3 let _dotbody = ".body" let _con = "con",3 @@ -92,6 +96,7 @@ let _con3 = "con" let _var3 = "var" let _ind3 = "ind" let _ann3 = "ann" +let _univ4 = "univ" let _types5 = "types" let _xpointer8 = "xpointer" let _cic5 = "cic:/" @@ -102,9 +107,11 @@ let is_malformed suri = else let len = String.length suri - 5 in let last5 = String.sub suri len 5 in + let last4 = String.sub last5 1 4 in let last3 = String.sub last5 2 3 in if last3 = _con3 || last3 = _var3 || last3 = _ind3 || - last3 = _ann3 || last5 = _types5 || last5 = _dotbody then + last3 = _ann3 || last5 = _types5 || last5 = _dotbody || + last4 = _univ4 then false else try @@ -177,9 +184,15 @@ let bodyuri_of_uri (uri, _) = None ;; +(* these are bugged! + * we should remove _types, _univ, _ann all toghether *) let innertypesuri_of_uri (uri, _) = uri_of_string ((clear_suffix uri _types) ^ _dottypes) ;; +let univgraphuri_of_uri (uri,_) = + uri_of_string ((clear_suffix uri _univ) ^ _dotuniv) +;; + let uri_of_uriref (uri, _) typeno consno = let typeno = typeno + 1 in