X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;h=6dad8ddef6c4095e4764497f21150d53c4e649e2;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=df707c956f2ba8f5e9de95d46480cf75d7cefdf9;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index df707c956..6dad8ddef 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -35,26 +35,6 @@ let name_of_uri uri = uri.(Array.length uri - 1);; let buri_of_uri uri = uri.(Array.length uri - 3);; let depth_of_uri uri = Array.length uri - 2;; -(*CSC: ora e' diventato poco efficiente, migliorare *) -let relative_depth curi uri cookingsno = - let rec length_of_current_prefix l1 l2 = - match (l1, l2) with - (he1::tl1, he2::tl2) when he1 == he2 -> - 1 + length_of_current_prefix tl1 tl2 - | (_,_) -> 0 - in - depth_of_uri uri - - length_of_current_prefix - (Array.to_list (Array.sub curi 0 (Array.length curi - (2 + cookingsno)))) - (Array.to_list (Array.sub uri 0 (Array.length uri - 2))) - (*CSC: vecchio codice da eliminare - if eq curi uri then 0 - else - depth_of_uri uri - - length_of_current_prefix (Array.to_list curi) (Array.to_list uri) - *) -;; - module OrderedStrings = struct type t = string