Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg

5 files changed, 29 insertions, 21 deletions

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] <filename>+ ]\n";
-  flush stderr;
+  eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\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);