Using same code for browsing physical directories in coqtop and coqdep.

In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
  ignoring silently and coqdep was exiting via handle_unix_error).

15 files changed, 174 insertions, 87 deletions

diff --git a/Makefile.build b/Makefile.build
index 0d87d98e9..6c3834ae4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -606,6 +606,7 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
 # coqdep_boot.
 
 COQDEPBOOTSRC:= \
+  lib/systemdirs.mli lib/systemdirs.ml \
   tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
   tools/coqdep_common.mli tools/coqdep_common.ml \
   tools/coqdep_boot.ml
diff --git a/Makefile.common b/Makefile.common
index d752a5be9..f83d8b88c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -232,7 +232,7 @@ IDEMOD:=$(shell cat ide/ide.mllib)
 
 # coqmktop, coqc
 
-COQENVCMO:=lib/clib.cma lib/errors.cmo
+COQENVCMO:=lib/clib.cma lib/errors.cmo lib/systemdirs.cmo
 
 COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 22df37562..8381144e8 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -33,6 +33,8 @@ Util
 Ephemeron
 Future
 CUnix
+
+Systemdirs
 System
 Profile
 RemoteCounter
diff --git a/checker/checker.ml b/checker/checker.ml
index ffe155319..360f99649 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -10,6 +10,7 @@ open Pp
 open Errors
 open Util
 open System
+open Systemdirs
 open Flags
 open Names
 open Check
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 2f78c2e91..7f8d4aad1 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -37,6 +37,7 @@ Util
 Bigint
 Dyn
 CUnix
+Systemdirs
 System
 Envars
 Aux_file
diff --git a/lib/lib.mllib b/lib/lib.mllib
index f3f6ad8fc..4730af32f 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,3 +1,4 @@
+Systemdirs
 Errors
 Bigint
 Dyn
diff --git a/lib/system.ml b/lib/system.ml
index 73095f9cd..6c01a270e 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -12,45 +12,27 @@ open Pp
 open Errors
 open Util
 open Unix
+open Systemdirs
 
-(* All subdirectories, recursively *)
-
-let exists_dir dir =
-  try let _ = closedir (opendir dir) in true with Unix_error _ -> false
-
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
-
-let ok_dirname f =
-  not (String.is_empty f) && f.[0] != '.' &&
-  not (String.List.mem f !skipped_dirnames) &&
-  (match Unicode.ident_refutation f with None -> true | _ -> false)
+(** Returns the list of all recursive subdirectories of [root] in
+    depth-first search, with sons ordered as on the file system;
+    warns if [root] does not exist *)
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
-  let rec traverse dir rel =
-    let dirh = opendir dir in
-    try
-      while true do
-	let f = readdir dirh in
-	if ok_dirname f then
-	  let file = Filename.concat dir f in
-	  try
-            begin match (stat file).st_kind with
-	    | S_DIR ->
-	      let newrel = rel @ [f] in
-	      add file newrel;
-	      traverse file newrel
-            | _ -> ()
-            end
-	  with Unix_error (e,s1,s2) -> ()
-      done
-    with End_of_file ->
-      closedir dirh
+  let rec traverse path rel =
+    let f = function
+      | FileDir (path,f) ->
+	  let newrel = rel @ [f] in
+	  add path newrel;
+	  traverse path newrel
+      | _ -> ()
+    in process_directory f path
   in
-  if exists_dir root then traverse root [];
+  check_unix_dir (fun s -> msg_warning (str s)) root;
+  if exists_dir root then traverse root []
+  else msg_warning (str ("Cannot open " ^ root));
   List.rev !l
 
 let rec search paths test =
diff --git a/lib/system.mli b/lib/system.mli
index a3d66d577..32a84f599 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -14,8 +14,6 @@
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)
 
-val exclude_search_in_dirname : string -> unit
-
 val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
 val is_in_path : CUnix.load_path -> string -> bool
 val is_in_system_path : string -> bool
@@ -24,8 +22,6 @@ val where_in_path :
 val where_in_path_rex :
   CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
 
-val exists_dir : string -> bool
-
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
diff --git a/lib/systemdirs.ml b/lib/systemdirs.ml
new file mode 100644
index 000000000..2275acd1b
--- /dev/null
+++ b/lib/systemdirs.ml
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Unix
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+  | FileDir of unix_path * (* basename of path: *) string 
+  | FileRegular of string (* basename of file *)
+
+(* Copy of Filename.concat but assuming paths to always be POSIX *)
+
+let (//) dirname filename =
+  let l = String.length dirname in
+  if l = 0 || dirname.[l-1] = '/'
+  then dirname ^ filename
+  else dirname ^ "/" ^ filename
+
+(* Excluding directories; We avoid directories starting with . as well
+   as CVS and _darcs and any subdirs given via -exclude-dir *)
+
+let skipped_dirnames = ref ["CVS"; "_darcs"]
+
+let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
+
+let ok_dirname f =
+  not (f = "") && f.[0] != '.' &&
+  not (List.mem f !skipped_dirnames) (*&&
+  (match Unicode.ident_refutation f with None -> true | _ -> false)*)
+
+(* Check directory can be opened *)
+
+let exists_dir dir =
+  try let _ = closedir (opendir dir) in true with Unix_error _ -> false
+
+let check_unix_dir warn dir =
+  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
+    (String.length dir > 2 && dir.[1] = ':' ||
+     String.contains dir '\\' ||
+     String.contains dir ';')
+  then warn ("assuming " ^ dir ^
+             " to be a Unix path even if looking like a Win32 path.")
+
+let apply_subdir f path name =
+  (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
+  (* as well as skipped files like CVS, ... *)
+  if name.[0] <> '.' && ok_dirname name then
+    let path = if path = "." then name else path//name in
+    match try (stat path).st_kind with Unix_error _ -> S_BLK with
+    | S_DIR -> f (FileDir (path,name))
+    | S_REG -> f (FileRegular name)
+    | _ -> ()
+
+let process_directory f path =
+  let dirh = opendir path in
+  try while true do apply_subdir f path (readdir dirh) done
+  with End_of_file -> closedir dirh
+
+let process_subdirectories f path =
+  let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
+  process_directory f path
+
diff --git a/lib/systemdirs.mli b/lib/systemdirs.mli
new file mode 100644
index 000000000..5d8d7ff9e
--- /dev/null
+++ b/lib/systemdirs.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+  | FileDir of unix_path * (* basename of path: *) string 
+  | FileRegular of string (* basename of file *)
+
+val (//) : unix_path -> string -> unix_path
+
+val exists_dir : unix_path -> bool
+
+(** [check_unix_dir warn path] calls [warn] with an appropriate
+     message if [path] looks does not look like a Unix path on Windows *)
+
+val check_unix_dir : (string -> unit) -> unix_path -> unit
+
+(** [exclude_search_in_dirname path] excludes [path] when processing
+    directories *)
+
+val exclude_directory : unix_path -> unit
+
+(** [process_directory f path] applies [f] on contents of directory
+    [path]; fails with Unix_error if the latter does not exists; skips
+    all files or dirs starting with "." *)
+
+val process_directory : (file_kind -> unit) -> unix_path -> unit
+
+(** [process_subdirectories f path] applies [f path/file file] on each
+    [file] of the directory [path]; fails with Unix_error if the
+    latter does not exists; kips all files or dirs starting with "." *)
+
+val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2e0cce6e5..57c9e82f2 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -9,6 +9,7 @@
 open Printf
 open Coqdep_lexer
 open Coqdep_common
+open Systemdirs
 
 (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
     are now in [Coqdep_common]. The code that remains here concerns
@@ -461,7 +462,7 @@ let rec parse = function
   | "-R" :: ([] | [_]) -> usage ()
   | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
   | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
-  | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll
+  | "-exclude-dir" :: r :: ll -> Systemdirs.exclude_directory r; parse ll
   | "-exclude-dir" :: [] -> usage ()
   | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
   | "-coqlib" :: [] -> usage ()
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2e6a15ceb..7f64949f9 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -9,6 +9,7 @@
 open Printf
 open Coqdep_lexer
 open Unix
+open Systemdirs
 
 (** [coqdep_boot] is a stripped-down version of [coqdep], whose
     behavior is the one of [coqdep -boot]. Its only dependencies
@@ -27,26 +28,11 @@ let option_boot = ref false
 let option_mldep = ref None
 
 let norec_dirs = ref ([] : string list)
-let norec_dirnames = ref ["CVS"; "_darcs"]
 
 let suffixe = ref ".vo"
 
 type dir = string option
 
-(* Filename.concat but always with a '/' *)
-let is_dir_sep s i =
-  match Sys.os_type with
-  | "Unix" -> s.[i] = '/'
-  | "Cygwin" | "Win32" ->
-    let c = s.[i] in c = '/' || c = '\\' || c = ':'
-  | _ -> assert false
-
-let (//) dirname filename =
-  let l = String.length dirname in
-  if l = 0 || is_dir_sep dirname (l-1)
-  then dirname ^ filename
-  else dirname ^ "/" ^ filename
-
 (** [get_extension f l] checks whether [f] has one of the extensions
     listed in [l]. It returns [f] without its extension, alongside with
     the extension. When no extension match, [(f,"")] is returned *)
@@ -165,6 +151,10 @@ let warning_clash file dir =
       eprintf "%s and %s; used the latter)\n" d2 d1
   | _ -> assert false
 
+let warning_cannot_open_dir dir =
+  eprintf "*** Warning: cannot open %s\n" dir;
+  flush stderr
+
 let safe_assoc verbose file k =
   if verbose && List.mem_assoc k !clash_v then warning_clash file k;
   Hashtbl.find vKnown k
@@ -463,42 +453,43 @@ let add_known recur phys_dir log_dir f =
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
-(* Visits all the directories under [dir], including [dir],
-   or just [dir] if [recur=false] *)
+(* Visits all the directories under [dir], including [dir] *)
 
-let rec add_directory recur add_file phys_dir log_dir =
-  let dirh = opendir phys_dir in
-  try
-    while true do
-      let f = readdir dirh in
-      (* we avoid all files and subdirs starting by '.' (e.g. .svn),
-         plus CVS and _darcs and any subdirs given via -exclude-dirs *)
-      if f.[0] <> '.' then
-        let phys_f = if phys_dir = "." then f else phys_dir//f in
-	match try (stat phys_f).st_kind with _ -> S_BLK with
-	  | S_DIR when recur ->
-              if List.mem f !norec_dirnames then ()
-              else
-	        if List.mem phys_f !norec_dirs then ()
-	        else
-		  add_directory recur add_file phys_f (log_dir@[f])
-	  | S_REG -> add_file phys_dir log_dir f
-	  | _ -> ()
-    done
-  with End_of_file -> closedir dirh
+let is_not_seen_directory phys_f =
+  not (List.mem phys_f !norec_dirs)
+
+let rec add_directory add_file phys_dir log_dir =
+  let f = function
+    | FileDir (phys_f,f) ->
+        if is_not_seen_directory phys_f then
+          add_directory add_file phys_f (log_dir @ [f])
+    | FileRegular f ->
+        add_file phys_dir log_dir f
+  in
+  Systemdirs.check_unix_dir (fun s -> eprintf "*** Warning: %s" s) phys_dir;
+  if exists_dir phys_dir then
+    process_directory f phys_dir
+  else
+    warning_cannot_open_dir phys_dir
 
 (** -Q semantic: go in subdirs but only full logical paths are known. *)
 let add_dir add_file phys_dir log_dir =
-  try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> ()
+  try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> ()
 
 (** -R semantic: go in subdirs and suffixes of logical paths are known. *)
 let add_rec_dir add_file phys_dir log_dir =
-  handle_unix_error (add_directory true (add_file true) phys_dir) log_dir
+  add_directory (add_file true) phys_dir log_dir
+
+(** -R semantic but only on immediate capitalized subdirs *)
+
+let add_rec_uppercase_subdirs add_file phys_dir log_dir =
+  process_subdirectories (fun phys_dir f ->
+    add_directory (add_file true) phys_dir (log_dir@[String.capitalize f]))
+    phys_dir
 
 (** -I semantic: do not go in subdirs. *)
 let add_caml_dir phys_dir =
-  handle_unix_error (add_directory true add_caml_known phys_dir) []
-
+  add_directory add_caml_known phys_dir []
 
 let rec treat_file old_dirname old_name =
   let name = Filename.basename old_name
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 71b96ca0e..d6065e4c2 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -6,16 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Systemdirs
+
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
 val option_natdynlk : bool ref
 val option_mldep : string option ref
 val norec_dirs : string list ref
-val norec_dirnames : string list ref
 val suffixe : string ref
 type dir = string option
-val ( // ) : string -> string -> string
 val get_extension : string -> string list -> string * string
 val basename_noext : string -> string
 val mlAccu : (string * string * dir) list ref
@@ -41,13 +41,12 @@ val coq_dependencies : unit -> unit
 val suffixes : 'a list -> 'a list list
 val add_known : bool -> string -> string list -> string -> unit
 val add_caml_known : string -> string list -> string -> unit
-val add_directory :
-  bool ->
-  (string -> string list -> string -> unit) -> string -> string list -> unit
 val add_caml_dir : string -> unit
 val add_dir :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 val add_rec_dir :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+val add_rec_uppercase_subdirs :
+  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 val treat_file : dir -> string -> unit
 val error_cannot_parse : string -> int * int -> 'a
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0b9bb2f2e..ffdd84619 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -455,7 +455,7 @@ let parse_args arglist =
     |"-compile-verbose" -> add_compile true (next ())
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
     |"-feedback-glob" -> Dumpglob.feedback_glob ()
-    |"-exclude-dir" -> exclude_search_in_dirname (next ())
+    |"-exclude-dir" -> Systemdirs.exclude_directory (next ())
     |"-init-file" -> set_rcfile (next ())
     |"-inputstate"|"-is" -> set_inputstate (next ())
     |"-load-ml-object" -> Mltop.dir_ml_load (next ())
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 357c5482f..ef2e62c3b 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -11,6 +11,7 @@ open Util
 open Pp
 open Flags
 open Libobject
+open Systemdirs
 open System
 
 (* Code to hook Coq into the ML toplevel -- depends on having the
@@ -155,7 +156,7 @@ let add_ml_dir s =
     | WithoutTop when has_dynlink -> keep_copy_mlpath s
     | _ -> ()
 
-(* For Rec Add ML Path *)
+(* For Rec Add ML Path (-R) *)
 let add_rec_ml_dir unix_path =
   List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path)