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). --- tools/coqdep_common.mli | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'tools/coqdep_common.mli') diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 71b96ca0ee..d6065e4c27 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,13 +41,12 @@ 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 -- cgit v1.2.3