From: Claudio Sacerdoti Coen Date: Thu, 26 Jun 2003 12:59:50 +0000 (+0000) Subject: relativeDepth function removed (useful only for cooking) X-Git-Tag: camera_ready~43 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d436761ba03acfadbfe913c0a38367068bdbb47;p=helm.git relativeDepth function removed (useful only for cooking) --- 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 diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 8afb4e345..0f4f15ea2 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -36,11 +36,6 @@ val name_of_uri : uri -> string (* name only (without extension)*) val buri_of_uri : uri -> string (* base uri only *) val depth_of_uri : uri -> int (* length of the path *) -(* relative_depth curi uri cookingsno *) -(* is the number of times to cook uri to use it when the current uri is curi *) -(* cooked cookingsno times *) -val relative_depth : uri -> uri -> int -> int - (* given an uri, returns the uri of the corresponding cic file, *) (* i.e. removes the [.types][.ann] suffix *) val cicuri_of_uri : uri -> uri