Vernacinterp et Vernacentries (partiellement)

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

4 files changed, 43 insertions, 3 deletions

diff --git a/lib/system.ml b/lib/system.ml
index ab24f734c7..0f005bd47f 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -27,6 +27,8 @@ let search_in_path path filename =
   in
   search path
 
+let where_in_path = search_in_path
+
 let find_file_in_path name =
   let globname = glob name in
   if not (Filename.is_relative globname) then
@@ -39,9 +41,35 @@ let find_file_in_path name =
 	(hOV 0 [< 'sTR"Can't find file" ; 'sPC ; 'sTR name ; 'sPC ; 
 		  'sTR"on loadpath" >])
 
+let is_in_path lpath filename =
+  try
+    let _ = search_in_path lpath filename in true
+  with
+    Not_found -> false
+
 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 6b773fdefc..6f89901aa5 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,15 +1,23 @@
 
 (* $Id$ *)
 
-(*s Files and load path. *)
+(*s Files. *)
+
+val alldir : string -> string list
+val is_in_path : string list -> string -> bool
+val where_in_path : string list -> string -> string
+
+val make_suffix : string -> string -> string
+
+val glob : string -> string
+
+(*s Global load path. *)
 
 val add_path : string -> unit
 val del_path : string -> unit
 
 val find_file_in_path : string -> string
 
-val make_suffix : string -> string -> string
-
 (*s Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
   when the check fails, with the full file name. *)
diff --git a/lib/util.ml b/lib/util.ml
index d165c157b2..ed56f06d76 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -49,6 +49,8 @@ let parse_section_path s =
   let id,k = decoupe_kind n in
   dirs,id,k
 
+module Stringset = Set.Make(struct type t = string let compare = compare end)
+
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
 let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
diff --git a/lib/util.mli b/lib/util.mli
index bcdf4493c6..506b63cbda 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -26,6 +26,8 @@ val implode : string list -> string
 
 val parse_section_path : string -> string list * string * string
 
+module Stringset : Set.S with type elt = string
+
 module Stringmap : Map.S with type key = string
 
 val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list