X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=3ee270e4e00b42fd0b012a512b11a92feef48c82;hb=b22ad9b6f6330602742ca300370c3ff57c6bb3e9;hp=24f0dd1967ab3f8711a5538f61058bcc13417fce;hpb=683978a2627cf1ce15673360f26806593d22f7b5;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 24f0dd196..3ee270e4e 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -422,3 +422,59 @@ let raise_localized_exception ~offset floc exn = let estimate_size x = 4 * (String.length (Marshal.to_string x [])) / 1024 +let normalize_path s = + let s = Str.global_replace (Str.regexp "//") "/" s in + let l = Str.split (Str.regexp "/") s in + let rec aux acc = function + | [] -> acc + | he::"."::tl -> aux acc (he::tl) + | he::".."::tl when he <> ".." -> aux [] (acc @ tl) + | he::tl -> aux (acc@[he]) tl + in + (if Str.string_match (Str.regexp "^/") s 0 then "/" else "") ^ + String.concat "/" (aux [] l) + ^ (if Str.string_match (Str.regexp "/$") s 0 then "/" else "") +;; + +let find_in paths path = + let rec aux = function + | [] -> raise (Failure "find_in") + | p :: tl -> + let path = normalize_path (p ^ "/" ^ path) in + try + if (Unix.stat path).Unix.st_kind = Unix.S_REG then path + else aux tl + with Unix.Unix_error _ as exn -> + aux tl + in + try + aux paths + with Unix.Unix_error _ | Failure _ -> + raise + (Failure "find_in") +;; + +let is_prefix_of_aux d1 d2 = + let len1 = String.length d1 in + let len2 = String.length d2 in + if len2 < len1 then + false, len1, len2 + else + let pref = String.sub d2 0 len1 in + pref = d1 && (len1 = len2 || d1.[len1-1] = '/' || d2.[len1] = '/'), len1, len2 + +let is_prefix_of d1 d2 = + let b,_,_ = is_prefix_of_aux d1 d2 in b +;; + +let chop_prefix prefix s = + let b,lp,ls = is_prefix_of_aux prefix s in + if b then + String.sub s lp (ls - lp) + else + s +;; + +let touch s = + try close_out(open_out s) with Sys_error _ -> () +;;