From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- lib/system.ml | 75 +++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 44 insertions(+), 31 deletions(-) (limited to 'lib/system.ml') diff --git a/lib/system.ml b/lib/system.ml index 94a57792..7d54e2c3 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* warning ("Cannot determine user home directory, using '.' ."); flush_all (); - "." + Filename.current_dir_name let safe_getenv n = safe_getenv_def n ("$"^n) @@ -72,20 +72,49 @@ type load_path = physical_path list let physical_path_of_string s = s let string_of_physical_path p = p +(* + * Split a path into a list of directories. A one-liner with Str, but Coq + * doesn't seem to use this library at all, so here is a slighly longer version. + *) + +let lpath_from_path path path_separator = + let n = String.length path in + let rec aux i l = + if i < n then + let j = + try String.index_from path i path_separator + with Not_found -> n + in + let dir = String.sub path i (j-i) in + aux (j+1) (dir::l) + else + l + in List.rev (aux 0 []) + (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) let n = String.length curdir in - if String.length p > n && String.sub p 0 n = curdir then - remove_path_dot (String.sub p n (String.length p - n)) + let l = String.length p in + if l > n && String.sub p 0 n = curdir then + let n' = + let sl = String.length Filename.dir_sep in + let i = ref n in + while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in + remove_path_dot (String.sub p n' (l - n')) else p let strip_path p = let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) let n = String.length cwd in - if String.length p > n && String.sub p 0 n = cwd then - remove_path_dot (String.sub p n (String.length p - n)) + let l = String.length p in + if l > n && String.sub p 0 n = cwd then + let n' = + let sl = String.length Filename.dir_sep in + let i = ref n in + while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in + remove_path_dot (String.sub p n' (l - n')) else remove_path_dot p @@ -179,6 +208,14 @@ let is_in_path lpath filename = try ignore (where_in_path ~warn:false lpath filename); true with Not_found -> false +let path_separator = if Sys.os_type = "Unix" then ':' else ';' + +let is_in_system_path filename = + let path = try Sys.getenv "PATH" + with Not_found -> error "system variable PATH not found" in + let lpath = lpath_from_path path path_separator in + is_in_path lpath filename + let make_suffix name suffix = if Filename.check_suffix name suffix then name else (name ^ suffix) @@ -300,34 +337,10 @@ let run_command converter f c = done; (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) -let path_separator = if Sys.os_type = "Unix" then ':' else ';' - -let search_exe_in_path exe = - try - let path = Sys.getenv "PATH" in - let n = String.length path in - let rec aux i = - if i < n then - let j = - try String.index_from path i path_separator - with Not_found -> n - in - let dir = String.sub path i (j-i) in - let exe = Filename.concat dir exe in - if Sys.file_exists exe then Some exe else aux (i+1) - else - None - in aux 0 - with Not_found -> None - (* Time stamps. *) type time = float * float * float -let process_time () = - let t = times () in - (t.tms_utime, t.tms_stime) - let get_time () = let t = times () in (time(), t.tms_utime, t.tms_stime) -- cgit v1.2.3