CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned

3 files changed, 96 insertions, 43 deletions

diff --git a/lib/cUnix.ml b/lib/cUnix.ml
index cecfcfb38b..a4d6903c02 100644
--- a/lib/cUnix.ml
+++ b/lib/cUnix.ml
@@ -18,30 +18,36 @@ let path_to_list p =
   let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in
     Str.split sep p
 
-(* Hints to partially detects if two paths refer to the same repertory *)
+(* Some static definitions concerning filenames *)
+
+let dirsep = Filename.dir_sep (* Unix: "/" *)
+let dirsep_len = String.length dirsep
+let curdir = Filename.concat Filename.current_dir_name "" (* Unix: "./" *)
+let curdir_len = String.length curdir
+
+(* Hints to partially detects if two paths refer to the same directory *)
+
+(** cut path [p] after all the [/] that come at position [pos]. *)
+let rec cut_after_dirsep p pos =
+  if CString.is_sub dirsep p pos then
+    cut_after_dirsep p (pos + dirsep_len)
+  else
+    String.sub p pos (String.length p - pos)
+
+(** remove all initial "./" in a path *)
 let rec remove_path_dot p =
-  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
-  let n = String.length curdir in
-  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'))
+  if CString.is_sub curdir p 0 then
+    remove_path_dot (cut_after_dirsep p curdir_len)
   else
     p
 
+(** If a path [p] starts with the current directory $PWD then
+    [strip_path p] returns the sub-path relative to $PWD.
+    Any leading "./" are also removed from the result. *)
 let strip_path p =
   let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
-  let n = String.length cwd in
-  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'))
+  if CString.is_sub cwd p 0 then
+    remove_path_dot (cut_after_dirsep p (String.length cwd))
   else
     remove_path_dot p
 
@@ -59,31 +65,54 @@ let canonical_path_name p =
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
-let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f
+let get_extension f =
+  let pos = try String.rindex f '.' with Not_found -> String.length f in
+  String.sub f pos (String.length f - pos)
+
+let correct_path f dir =
+  if Filename.is_relative f then Filename.concat dir f else f
 
 let file_readable_p name =
-  try Unix.access name [Unix.R_OK];true with Unix.Unix_error (_, _, _) -> false
+  try Unix.access name [Unix.R_OK];true
+  with Unix.Unix_error (_, _, _) -> false
 
-let run_command converter f c =
+(* As for [Unix.close_process], a [Unix.waipid] that ignores all [EINTR] *)
+
+let rec waitpid_non_intr pid =
+  try snd (Unix.waitpid [] pid)
+  with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid
+
+(** [run_command com] launches command [com] (via /bin/sh),
+    and returns the contents of stdout and stderr. If given, [~hook]
+    is called on each elements read on stdout or stderr. *)
+
+let run_command ?(hook=(fun _ ->())) c =
   let result = Buffer.create 127 in
   let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
   let buff = String.make 127 ' ' in
   let buffe = String.make 127 ' ' in
   let n = ref 0 in
   let ne = ref 0 in
-
   while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ;
     !n+ !ne <> 0
   do
-    let r = converter (String.sub buff 0 !n) in
-    f r;
-    Buffer.add_string result r;
-    let r = converter (String.sub buffe 0 !ne) in
-    f r;
-    Buffer.add_string result r
+    let r = String.sub buff 0 !n in (hook r; Buffer.add_string result r);
+    let r = String.sub buffe 0 !ne in (hook r; Buffer.add_string result r);
   done;
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
+(** [sys_command] launches program [prog] with arguments [args].
+    It behaves like [Sys.command], except that we rely on
+    [Unix.create_process], it's hardly more complex and avoids dealing
+    with shells. In particular, no need to quote arguments
+    (against whitespace or other funny chars in paths), hence no need
+    to care about the different quoting conventions of /bin/sh and cmd.exe. *)
+
+let sys_command prog args =
+  let argv = Array.of_list (prog::args) in
+  let pid = Unix.create_process prog argv Unix.stdin Unix.stdout Unix.stderr in
+  waitpid_non_intr pid
+
 (*
   checks if two file names refer to the same (existing) file by
   comparing their device and inode.
diff --git a/lib/cUnix.mli b/lib/cUnix.mli
index c6118c4c56..9ba1cd8539 100644
--- a/lib/cUnix.mli
+++ b/lib/cUnix.mli
@@ -11,29 +11,55 @@
 type physical_path = string
 type load_path = physical_path list
 
+val physical_path_of_string : string -> physical_path
+val string_of_physical_path : physical_path -> string
+
 val canonical_path_name : string -> string
+
+(** remove all initial "./" in a path *)
 val remove_path_dot : string -> string
+
+(** If a path [p] starts with the current directory $PWD then
+    [strip_path p] returns the sub-path relative to $PWD.
+    Any leading "./" are also removed from the result. *)
 val strip_path : string -> string
+
 (** correct_path f dir = dir/f if f is relative *)
 val correct_path : string -> string -> string
 
-
-val physical_path_of_string : string -> physical_path
-val string_of_physical_path : physical_path -> string
-
 val path_to_list : string -> string list
 
+(** [make_suffix file suf] catenate [file] with [suf] when
+    [file] does not already end with [suf]. *)
 val make_suffix : string -> string -> string
+
+(** Return the extension of a file, i.e. its smaller suffix starting
+    with "." if any, or "" otherwise. *)
+val get_extension : string -> string
+
 val file_readable_p : string -> bool
 
 (** {6 Executing commands } *)
-(** [run_command converter f com] launches command [com], and returns
-    the contents of stdout and stderr that have been processed with
-    [converter]; the processed contents of stdout and stderr is also
-    passed to [f] *)
 
-val run_command : (string -> string) -> (string -> unit) -> string ->
-  Unix.process_status * string
+(** [run_command com] launches command [com], and returns
+    the contents of stdout and stderr. If given, [~hook]
+    is called on each elements read on stdout or stderr. *)
+
+val run_command :
+  ?hook:(string->unit) -> string -> Unix.process_status * string
+
+(** [sys_command] launches program [prog] with arguments [args].
+    It behaves like [Sys.command], except that we rely on
+    [Unix.create_process], it's hardly more complex and avoids dealing
+    with shells. In particular, no need to quote arguments
+    (against whitespace or other funny chars in paths), hence no need
+    to care about the different quoting conventions of /bin/sh and cmd.exe. *)
+
+val sys_command : string -> string list -> Unix.process_status
+
+(** A version of [Unix.waitpid] immune to EINTR exceptions *)
+
+val waitpid_non_intr : int -> Unix.process_status
 
 (** checks if two file names refer to the same (existing) file *)
 val same_file : string -> string -> bool
diff --git a/lib/envars.ml b/lib/envars.ml
index 5e20df3585..0247058218 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -155,11 +155,10 @@ let ocamlc () = camlbin () / Coq_config.ocamlc
 let ocamlopt () = camlbin () / Coq_config.ocamlopt
 
 let camllib () =
-  if !Flags.boot then 
+  if !Flags.boot then
     Coq_config.camllib
   else
-    let com = ocamlc () ^ " -where" in
-    let _, res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
+    let _, res = CUnix.run_command (ocamlc () ^ " -where") in
     String.strip res
 
 (** {2 Camlp4 paths} *)
@@ -181,8 +180,7 @@ let camlp4lib () =
   if !Flags.boot then 
     Coq_config.camlp4lib
   else
-    let com = camlp4 () ^ " -where" in
-    let ex, res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
+    let ex, res = CUnix.run_command (camlp4 () ^ " -where") in
     match ex with
       | Unix.WEXITED 0 -> String.strip res
       | _ -> "/dev/null"