poursuite de Vernacentries

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

6 files changed, 55 insertions, 21 deletions

diff --git a/lib/options.ml b/lib/options.ml
index c4afa1e390..c0f14ee30b 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -1,6 +1,8 @@
 
 (* $Id$ *)
 
+open Util
+
 let batch_mode = ref false
 
 let debug = ref false
@@ -41,3 +43,10 @@ let without_mes_ambig f x =
   try make_mes_ambig false;
       let rslt = f x in (make_mes_ambig old; rslt)
   with e -> (make_mes_ambig old; raise e)
+
+(* A list of the areas of the system where "unsafe" operation
+ * has been requested *)
+let unsafe_set = ref Stringset.empty
+let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
+let is_unsafe s = Stringset.mem s !unsafe_set
+
diff --git a/lib/options.mli b/lib/options.mli
index 528226360e..9137883523 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -22,3 +22,6 @@ val make_mes_ambig : bool -> unit
 val is_mes_ambig : unit -> bool
 val without_mes_ambig : ('a -> 'b) -> 'a -> 'b
 
+val add_unsafe : string -> unit
+val is_unsafe : string -> bool
+
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)
diff --git a/lib/system.mli b/lib/system.mli
index 6f89901aa5..0c4bbd2284 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -3,7 +3,7 @@
 
 (*s Files. *)
 
-val alldir : string -> string list
+val all_subdirs : string -> string list
 val is_in_path : string list -> string -> bool
 val where_in_path : string list -> string -> string
 
@@ -15,6 +15,9 @@ val glob : string -> string
 
 val add_path : string -> unit
 val del_path : string -> unit
+val radd_path : string -> unit
+
+val search_paths : unit -> string list
 
 val find_file_in_path : string -> string
 
diff --git a/lib/util.ml b/lib/util.ml
index 59f119a50c..0cab4540e2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -207,6 +207,12 @@ let list_map_append f l = List.flatten (List.map f l)
 
 let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
 
+let list_share_tails l1 l2 =
+  let rec shr_rev acc = function
+    | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2)
+    | (l1,l2) -> (List.rev l1, List.rev l2, acc)
+  in 
+  shr_rev [] (List.rev l1, List.rev l2)
 
 (* Arrays *)
 
diff --git a/lib/util.mli b/lib/util.mli
index b8b72da090..a3a20aaacf 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -62,6 +62,7 @@ val list_prefix_of : 'a list -> 'a list -> bool
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 (* raises [Invalid_argument] if the two lists don't have the same length *)
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
 
 (*s Arrays. *)