poursuite de Vernacentries

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@178 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 32 insertions, 20 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 0f005bd47f..9da302d302 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -3,6 +3,7 @@
 
 open Pp
 open Util
+open Unix
 
 (* Files and load path. *)
 
@@ -14,6 +15,37 @@ let del_path dir =
   if List.mem dir !load_path then
     load_path := List.filter (fun s -> s <> dir) !load_path
 
+let search_paths () = !load_path
+
+(* All subdirectories, recursively *)
+
+let all_subdirs dir =
+  let l = ref [] in
+  let add f = l := f :: !l in
+  let rec traverse dir =
+    Printf.printf "%s\n" dir;
+    let dirh = 
+      try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" 
+    in
+    try
+      while true do
+	let f = readdir dirh in
+	if f <> "." && f <> ".." then
+	  let file = Filename.concat dir f in
+	  if (stat file).st_kind = S_DIR then begin
+	    add file;
+	    traverse file
+	  end
+      done
+    with End_of_file ->
+      closedir dirh
+  in
+  traverse dir; List.rev !l
+
+let radd_path dir = List.iter add_path (all_subdirs dir)
+
+
+
 (* TODO: rétablir glob (expansion ~user et $VAR) si on le juge nécessaire *)
 let glob s = s
 
@@ -50,26 +82,6 @@ let is_in_path lpath filename =
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
-(*Gives the list of all the directories under dir*)
-let alldir dir =
-  let ini = Unix.getcwd()
-  and tmp = Filename.temp_file "coq" "rec"
-  and lst = ref [] in
-  Unix.chdir dir;
-  let bse = Unix.getcwd() in
-  let _ = Sys.command ("find "^bse^" -type d >> "^tmp) in
-  let inf = open_in tmp in
-  try
-    while true do
-      lst := !lst @ [input_line inf]
-    done;
-    []
-  with End_of_file ->
-    close_in inf;
-    Sys.remove tmp;
-    Unix.chdir ini;
-    !lst
-
 let open_trapping_failure open_fun name suffix =
   let rname = make_suffix name suffix in
   try open_fun rname with _ -> error ("Can't open " ^ rname)