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

(Sorry, was not intended to be pushed)

This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.

5 files changed, 37 insertions, 127 deletions

diff --git a/lib/lib.mllib b/lib/lib.mllib
index 4730af32f..f3f6ad8fc 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 6c01a270e..73095f9cd 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 32a84f599..a3d66d577 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 2275acd1b..000000000
--- 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 5d8d7ff9e..000000000
--- 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