From de8888e28ad793511ba2e2969516325b0be44330 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 12 Feb 2015 18:52:09 +0100 Subject: Revert "Using same code for browsing physical directories in coqtop and coqdep." (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. --- lib/lib.mllib | 1 - lib/system.ml | 48 +++++++++++++++++++++++++------------ lib/system.mli | 4 ++++ lib/systemdirs.ml | 70 ------------------------------------------------------ lib/systemdirs.mli | 41 -------------------------------- 5 files changed, 37 insertions(+), 127 deletions(-) delete mode 100644 lib/systemdirs.ml delete mode 100644 lib/systemdirs.mli (limited to 'lib') 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 *) -(* 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 *) -(* 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 -- cgit v1.2.3