From 5268efdefb396267bfda0c17eb045fa2ed516b3c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 31 Jan 2015 09:09:28 +0100 Subject: 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). --- lib/lib.mllib | 1 + lib/system.ml | 48 ++++++++++++------------------------- lib/system.mli | 4 ---- lib/systemdirs.ml | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/systemdirs.mli | 41 ++++++++++++++++++++++++++++++++ 5 files changed, 127 insertions(+), 37 deletions(-) create mode 100644 lib/systemdirs.ml create mode 100644 lib/systemdirs.mli (limited to 'lib') diff --git a/lib/lib.mllib b/lib/lib.mllib index f3f6ad8fc7..4730af32f6 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 73095f9cd6..6c01a270e2 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 a3d66d577a..32a84f5996 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 0000000000..2275acd1b1 --- /dev/null +++ b/lib/systemdirs.ml @@ -0,0 +1,70 @@ +(************************************************************************) +(* 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 new file mode 100644 index 0000000000..5d8d7ff9eb --- /dev/null +++ b/lib/systemdirs.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* 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