From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- tools/coqdep.ml | 13 ++++++++----- tools/coqdep_boot.ml | 2 +- tools/coqdep_common.ml | 16 ++++++++++------ tools/coqdep_common.mli | 3 ++- tools/fake_ide.ml | 16 ++++++++-------- 5 files changed, 29 insertions(+), 21 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 90cdd12d..8a5f0695 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -157,9 +157,10 @@ let declare_dependencies () = (List.rev !vAccu) let usage () = - eprintf - "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] + ]\n"; - flush stderr; + eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] +\n"; + eprintf " extra options:\n"; + eprintf " -coqlib dir : set the coq standard library directory\n"; + eprintf " -exclude-dir f : skip subdirectories named f during -R search\n"; exit 1 let rec parse = function @@ -177,9 +178,11 @@ let rec parse = function | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll | "-R" :: ([] | [_]) -> usage () - | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll + | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: [] -> usage () + | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: (s :: ll) -> suffixe := s ; parse ll + | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () | "-slash" :: ll -> option_slash := true; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 19aba41d..15fcdc60 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -26,7 +26,7 @@ let rec parse = function (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_dir add_known r []; - norecdir_list:=r::!norecdir_list; + norec_dirs:=r::!norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 4977a94c..2b316b0c 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -26,7 +26,8 @@ let option_slash = ref false let option_natdynlk = ref true let option_mldep = ref None -let norecdir_list = ref ([]:string list) +let norec_dirs = ref ([] : string list) +let norec_dirnames = ref ["CVS"; "_darcs"] let suffixe = ref ".vo" @@ -439,14 +440,17 @@ let rec add_directory recur add_file phys_dir log_dir = try while true do let f = readdir dirh in - (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *) - if f.[0] <> '.' && f.[0] <> '_' then + (* we avoid all files and subdirs starting by '.' (e.g. .svn), + plus CVS and _darcs and any subdirs given via -exclude-dirs *) + if f.[0] <> '.' then let phys_f = if phys_dir = "." then f else phys_dir//f in match try (stat phys_f).st_kind with _ -> S_BLK with | S_DIR when recur -> - if List.mem phys_f !norecdir_list then () - else - add_directory recur add_file phys_f (log_dir@[f]) + if List.mem f !norec_dirnames then () + else + if List.mem phys_f !norec_dirs then () + else + add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f | _ -> () done diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index afc171cb..d9ca3ca8 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -11,7 +11,8 @@ val option_noglob : bool ref val option_slash : bool ref val option_natdynlk : bool ref val option_mldep : string option ref -val norecdir_list : string list 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 diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 22a36ede..7b688212 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -26,15 +26,15 @@ let eval_call (call:'a Ide_intf.call) = match res with Interface.Fail _ -> exit 1 | _ -> () let commands = - [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s))); - "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s))); - "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s))); - "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s))); + [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (0,true,false,s))); + "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (0,true,true,s))); + "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (0,false,false,s))); + "INTERP", (fun s -> eval_call (Ide_intf.interp (0,false,true,s))); "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s))); - "GOALS", (fun _ -> eval_call Ide_intf.goals); - "HINTS", (fun _ -> eval_call Ide_intf.hints); - "GETOPTIONS", (fun _ -> eval_call Ide_intf.get_options); - "STATUS", (fun _ -> eval_call Ide_intf.status); + "GOALS", (fun _ -> eval_call (Ide_intf.goals ())); + "HINTS", (fun _ -> eval_call (Ide_intf.hints ())); + "GETOPTIONS", (fun _ -> eval_call (Ide_intf.get_options ())); + "STATUS", (fun _ -> eval_call (Ide_intf.status ())); "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s)); "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s)); "#", (fun _ -> raise Comment); -- cgit v1.2.3