X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fextlib%2FhExtlib.ml;h=a0f9d8d6cbb1ab0295b65035f873c724e6668d5d;hb=5dd5b3f6cd990d4d126b44c092e1df7f86c506d4;hp=c09dcf2c10fefc0f8fd6b51dc1ee7b05d8b1cfd4;hpb=7cf9117b7c5f6c322c8b02044f4548fae13d0653;p=helm.git diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index c09dcf2c1..a0f9d8d6c 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -26,11 +26,15 @@ (** PROFILING *) +(* we should use a key in te registry, but we can't see the registry.. *) let profiling_enabled = true +let profiling_printings = ref (fun () -> true) +let set_profiling_printings f = profiling_printings := f + type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } let profile ?(enable = true) = - if profiling_enabled && enable then + if profiling_enabled && enable then function s -> let total = ref 0.0 in let profile f x = @@ -48,8 +52,9 @@ let profile ?(enable = true) = in at_exit (fun () -> - print_endline - ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); + if !profiling_printings () then + prerr_endline + ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total)); { profile = profile } else function _ -> { profile = fun f x -> f x } @@ -107,11 +112,11 @@ let is_alphanum c = is_alpha c || is_digit c (** {2 List processing} *) -let rec list_uniq = function +let rec list_uniq ?(eq=(=)) = function | [] -> [] | h::[] -> [h] - | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) - | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl + | h1::h2::tl when eq h1 h2 -> list_uniq ~eq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq ~eq tl let rec filter_map f = function @@ -267,6 +272,27 @@ let find ?(test = fun _ -> true) path = in aux [] [path] +let safe_remove fname = if Sys.file_exists fname then Sys.remove fname + +let is_dir_empty d = + let od = Unix.opendir d in + let rec aux () = + let name = Unix.readdir od in + if name <> "." && name <> ".." then false else aux () in + let res = try aux () with End_of_file -> true in + Unix.closedir od; + res + +let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> () + +let rec rmdir_descend d = + if is_dir_empty d then + begin + safe_rmdir d; + rmdir_descend (Filename.dirname d) + end + + (** {2 Exception handling} *) let finally at_end f arg = @@ -277,3 +303,20 @@ let finally at_end f arg = at_end (); res +(** {2 Localized exceptions } *) + +exception Localized of Token.flocation * exn + +let loc_of_floc = function + | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> + (loc_begin, loc_end) + +let raise_localized_exception ~offset floc exn = + 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 + raise (Localized (floc, exn))