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

(Sorry, was not intended to be pushed)

This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.

15 files changed, 87 insertions, 174 deletions

diff --git a/Makefile.build b/Makefile.build
index 6c3834ae43..0d87d98e96 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -606,7 +606,6 @@ 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 f83d8b88c6..d752a5be91 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 lib/systemdirs.cmo
+COQENVCMO:=lib/clib.cma lib/errors.cmo
 
 COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 8381144e89..22df375623 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -33,8 +33,6 @@ Util
 Ephemeron
 Future
 CUnix
-
-Systemdirs
 System
 Profile
 RemoteCounter
diff --git a/checker/checker.ml b/checker/checker.ml
index 360f996499..ffe1553197 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -10,7 +10,6 @@ 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 7f8d4aad16..2f78c2e915 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -37,7 +37,6 @@ Util
 Bigint
 Dyn
 CUnix
-Systemdirs
 System
 Envars
 Aux_file
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 4730af32f6..f3f6ad8fc7 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,4 +1,3 @@
-Systemdirs
 Errors
 Bigint
 Dyn
diff --git a/lib/system.ml b/lib/system.ml
index 6c01a270e2..73095f9cd6 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -12,27 +12,45 @@ open Pp
 open Errors
 open Util
 open Unix
-open Systemdirs
 
-(** 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 *)
+(* 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)
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
-  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
+  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
   in
-  check_unix_dir (fun s -> msg_warning (str s)) root;
-  if exists_dir root then traverse root []
-  else msg_warning (str ("Cannot open " ^ root));
+  if exists_dir root then traverse root [];
   List.rev !l
 
 let rec search paths test =
diff --git a/lib/system.mli b/lib/system.mli
index 32a84f5996..a3d66d577a 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -14,6 +14,8 @@
     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
@@ -22,6 +24,8 @@ 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
deleted file mode 100644
index 2275acd1b1..0000000000
--- a/lib/systemdirs.ml
+++ /dev/null
@@ -1,70 +0,0 @@
-(************************************************************************)
-(*  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
deleted file mode 100644
index 5d8d7ff9eb..0000000000
--- a/lib/systemdirs.mli
+++ /dev/null
@@ -1,41 +0,0 @@
-(************************************************************************)
-(*  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 57c9e82f22..2e0cce6e53 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -9,7 +9,6 @@
 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
@@ -462,7 +461,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 -> Systemdirs.exclude_directory r; parse ll
+  | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; 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 7f64949f92..2e6a15cebd 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -9,7 +9,6 @@
 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
@@ -28,11 +27,26 @@ 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 *)
@@ -151,10 +165,6 @@ 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
@@ -453,43 +463,42 @@ 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] *)
-
-let is_not_seen_directory phys_f =
-  not (List.mem phys_f !norec_dirs)
+(* Visits all the directories under [dir], including [dir],
+   or just [dir] if [recur=false] *)
 
-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
+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
 
 (** -Q semantic: go in subdirs but only full logical paths are known. *)
 let add_dir add_file phys_dir log_dir =
-  try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> ()
+  try add_directory true (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 =
-  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
+  handle_unix_error (add_directory true (add_file true) phys_dir) log_dir
 
 (** -I semantic: do not go in subdirs. *)
 let add_caml_dir phys_dir =
-  add_directory add_caml_known phys_dir []
+  handle_unix_error (add_directory true 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 d6065e4c27..71b96ca0ee 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,12 +41,13 @@ 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 ffdd846197..0b9bb2f2ee 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" -> Systemdirs.exclude_directory (next ())
+    |"-exclude-dir" -> exclude_search_in_dirname (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 ef2e62c3b5..357c5482fd 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -11,7 +11,6 @@ open Util
 open Pp
 open Flags
 open Libobject
-open Systemdirs
 open System
 
 (* Code to hook Coq into the ML toplevel -- depends on having the
@@ -156,7 +155,7 @@ let add_ml_dir s =
     | WithoutTop when has_dynlink -> keep_copy_mlpath s
     | _ -> ()
 
-(* For Rec Add ML Path (-R) *)
+(* For Rec Add ML Path *)
 let add_rec_ml_dir unix_path =
   List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path)