modules Bij, Gmapl, Stock

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

2 files changed, 25 insertions, 0 deletions

diff --git a/library/library.ml b/library/library.ml
index 1f040984ac..6edc044a4b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Environ
@@ -43,6 +44,16 @@ let module_is_loaded s =
 let module_is_opened s =
   (find_module s).module_opened
 
+let loaded_modules () =
+  let l = ref [] in
+  Hashtbl.iter (fun s _ -> l := s :: !l) modules_table;
+  !l
+
+let opened_modules () =
+  let l = ref [] in
+  Hashtbl.iter (fun s m -> if m.module_opened then l := s :: !l) modules_table;
+  !l
+
 let vo_magic_number = 0700
 
 let (raw_extern_module, raw_intern_module) =
@@ -149,3 +160,12 @@ let save_module_to s f =
   close_out ch
 
 
+(* Pretty-printing of modules state. *)
+
+let fmt_modules_state () =
+  let opened = opened_modules ()
+  and loaded = loaded_modules () in
+  [< 'sTR "Imported (open) Modules: " ;
+     prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) opened ; 'fNL ;
+     'sTR "Loaded Modules: " ;
+     prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) loaded ; 'fNL >]
diff --git a/library/library.mli b/library/library.mli
index dc34de8a07..f3899250ee 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -14,6 +14,11 @@ val open_module : string -> unit
 val module_is_loaded : string -> bool
 val module_is_opened : string -> bool
 
+val loaded_modules : unit -> string list
+val opened_modules : unit -> string list
+
+val fmt_modules_state : unit -> Pp.std_ppcmds
+
 (*s Require. The command [require_module spec m file export] loads and opens
   a module [m]. [file] specifies the filename, if not [None]. [spec]
   specifies to look for a specification ([true]) or for an implementation