]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/extlib/hExtlib.ml
added list_mapi
[helm.git] / helm / software / components / extlib / hExtlib.ml
index 3ee270e4e00b42fd0b012a512b11a92feef48c82..fe587e297c50b5631d992852e12b2ae9bc84486c 100644 (file)
@@ -27,7 +27,7 @@
 
 (** PROFILING *)
 
-let profiling_enabled = false ;; (* ComponentsConf.profiling *)
+let profiling_enabled = ref false ;; (* 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;
@@ -139,6 +140,14 @@ let flatten_map f l =
   List.flatten (List.map f l)
 ;;
 
+let list_mapi f l =
+  let rec aux k = function
+    | [] -> []
+    | h::tl -> f h k :: aux (k+1) tl
+  in
+     aux 0 l
+;;
+
 let rec list_uniq ?(eq=(=)) = function 
   | [] -> []
   | h::[] -> [h]
@@ -444,7 +453,7 @@ let find_in paths path =
        try
          if (Unix.stat path).Unix.st_kind = Unix.S_REG then path
          else aux tl
-       with Unix.Unix_error _ as exn -> 
+       with Unix.Unix_error _ -> 
                aux tl
    in
    try