diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 20 | ||||
| -rw-r--r-- | library/library.mli | 5 |
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 |