diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-31 09:09:28 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-16 12:31:59 +0100 |
commit | 1be9c4da4d814c29d4ba45b121fda924adc1130e (patch) | |
tree | d20c6b62a97db66ce5784fe32a8f971e296b0738 /lib/system.mli | |
parent | 48d611ff2a60131369a66924e8d54f8e7c4ad911 (diff) |
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),
- uniformly expecting paths in Unix format and warning otherwise.
Diffstat (limited to 'lib/system.mli')
-rw-r--r-- | lib/system.mli | 38 |
1 files changed, 34 insertions, 4 deletions
diff --git a/lib/system.mli b/lib/system.mli index a3d66d577..6ed450326 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -8,14 +8,46 @@ (** {5 Coqtop specific system utilities} *) +(** {6 Directories} *) + +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 + (** {6 Files and load paths} *) (** Load path entries remember the original root 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 +56,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 |