X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=0d7254c8bd48cd34b8374e11f6c224d3620213a8;hb=4b5527a6ccbe73ada47f903292959ed3dde3b5c6;hp=073c5695959480e657070af45a68ec3029132ef6;hpb=137a822662f81efbbeac7ddc833fc9ffe252a70e;p=helm.git

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 073c56959..0d7254c8b 100644
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -27,7 +27,7 @@
 
 (** PROFILING *)
 
-let profiling_enabled = false ;; (* ComponentsConf.profiling *)
+let profiling_enabled = ref true ;; (* ComponentsConf.profiling *)
 
 let something_profiled = ref false
 
@@ -47,11 +47,12 @@ let set_profiling_printings f = profiling_printings := f
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }
 let profile ?(enable = true) s =
- if profiling_enabled && enable then
+ if !profiling_enabled && enable then
    let total = ref 0.0 in
    let calls = ref 0 in
    let max = ref 0.0 in
    let profile f x =
+    if not !profiling_enabled then f x else
     let before = Unix.gettimeofday () in
     try
      incr calls;
@@ -214,11 +215,31 @@ let is_dir fname =
     (Unix.stat fname).Unix.st_kind = Unix.S_DIR
   with Unix.Unix_error _ -> false
 
+let writable_dir path =
+  try
+    let file = path ^ "/prova_matita" in
+    let oc = open_out file in
+    close_out oc;
+    Sys.remove file;
+    true
+  with Sys_error _ -> false
+
+
 let is_regular fname =
   try
     (Unix.stat fname).Unix.st_kind = Unix.S_REG
   with Unix.Unix_error _ -> false
 
+let is_executable fname =
+  try
+    let stat = (Unix.stat fname) in
+    stat.Unix.st_kind = Unix.S_REG &&
+    (stat.Unix.st_perm land 0o001 > 0)
+  with Unix.Unix_error _ -> false
+
+let chmod mode filename =
+   Unix.chmod filename mode
+
 let mkdir path =
   let components = split ~sep:'/' path in
   let rec aux where = function
@@ -227,13 +248,13 @@ let mkdir path =
         let path =
           if where = "" then piece else where ^ "/" ^ piece in
         (try
-          Unix.mkdir path 0o755
+          Unix.mkdir path 0o755; chmod 0o2775 path 
         with 
         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
         | Unix.Unix_error (e,_,_) -> 
             raise 
               (Failure 
-                ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
+                ("Unix.mkdir " ^ path ^ " 0o2775 :" ^ (Unix.error_message e))));
         aux path tl
   in
   let where = if path.[0] = '/' then "/" else "" in
@@ -265,7 +286,8 @@ let input_all ic =
 let output_file ~filename ~text = 
   let oc = open_out filename in
   output_string oc text;
-  close_out oc
+  close_out oc;
+  chmod 0o664 filename
 
 let blank_split s =
   let len = String.length s in
@@ -382,32 +404,78 @@ let finally at_end f arg =
 
 (** {2 Localized exceptions } *)
 
-exception Localized of Token.flocation * exn
+exception Localized of Stdpp.location * exn
 
-let loc_of_floc = function
-  | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
-      (loc_begin, loc_end)
+let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;;
 
 let floc_of_loc (loc_begin, loc_end) =
-  let floc_begin =
-    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
-      Lexing.pos_cnum = loc_begin }
-  in
-  let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
-  (floc_begin, floc_end)
+ Stdpp.make_loc (loc_begin, loc_end)
 
 let dummy_floc = floc_of_loc (-1, -1)
 
 let raise_localized_exception ~offset floc exn =
- let (x, y) = loc_of_floc floc in
+ let x, y = loc_of_floc floc in
  let x = offset + x in
  let y = offset + y in
- let flocb,floce = floc in
- let floc =
-   { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y }
- in
+ let floc = floc_of_loc (x,y) in
   raise (Localized (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 _ -> 
+               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 _ -> ()
+;;