module_segment et module_filename

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

1 files changed, 18 insertions, 19 deletions

diff --git a/library/library.ml b/library/library.ml
index 3bd19dc1a9..d3af390712 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -8,8 +8,7 @@ open Environ
 open Libobject
 open Lib
 
-(* Modules on disk contain the following informations (after the magic 
-   number, and before the digest). *)
+(*s This generates commands Add Path, Remove Path, Print Path *)
 
 let loadpath_name = "LoadPath"
 
@@ -24,7 +23,6 @@ struct
   let synchronous = false
 end
 
-(* This generates commands Add Path, Remove Path, Print Path *)
 module LoadPathTable = Goptions.MakeStringTable(LoadPath)
 
 let get_load_path = LoadPathTable.elements
@@ -34,15 +32,8 @@ let remove_path dir =
   (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#remove dir
 let rec_add_path dir = List.iter add_path (System.all_subdirs dir)
 
-(* Vieilles versions
-let load_path = ref ([] : string list)
-let add_path dir = load_path := dir :: !load_path
-let remove_path dir =
-  if List.mem dir !load_path then
-    load_path := List.filter (fun s -> s <> dir) !load_path
-let get_load_path () = !load_path
-let rec_add_path dir = List.iter add_path (System.all_subdirs dir)
-*)
+(*s Modules on disk contain the following informations (after the magic 
+    number, and before the digest). *)
 
 type module_disk = { 
   md_name : string;
@@ -50,11 +41,12 @@ type module_disk = {
   md_declarations : library_segment;
   md_deps : (string * Digest.t * bool) list }
 
-(* Modules loaded in memory contain the following informations. They are
-   kept in the hash table [modules_table]. *)
+(*s Modules loaded in memory contain the following informations. They are
+    kept in the global table [modules_table]. *)
 
 type module_t = {
   module_name : string;
+  module_filename : string;
   module_compiled_env : compiled_env;
   module_declarations : library_segment;
   mutable module_opened : bool;
@@ -88,6 +80,12 @@ let opened_modules () =
   Stringmap.fold (fun s m l -> if m.module_opened then s :: l else l) 
     !modules_table []
 
+let module_segment = function
+  | None -> contents_after None
+  | Some m -> (find_module m).module_declarations
+
+let module_filename m = (find_module m).module_filename
+
 let vo_magic_number = 0700
 
 let (raw_extern_module, raw_intern_module) =
@@ -105,7 +103,7 @@ let segment_iter f =
   iter
 
 
-(* [open_module s] opens a module which is assumed to be already loaded. *)
+(*s [open_module s] opens a module which is assumed to be already loaded. *)
 
 let open_module s =
   let m = find_module s in
@@ -115,7 +113,7 @@ let open_module s =
   end
 
 
-(* [load_module s] loads the module [s] from the disk, and [find_module s]
+(*s [load_module s] loads the module [s] from the disk, and [find_module s]
    returns the module of name [s], loading it if necessary. 
    The boolean [doexp] specifies if we open the modules which are declared
    exported in the dependencies (usually it is [true] at the highest level;
@@ -130,6 +128,7 @@ let rec load_module_from doexp s f =
   let digest = System.marshal_in ch in
   close_in ch;
   let m = { module_name = md.md_name;
+	    module_filename = fname;
 	    module_compiled_env = md.md_compiled_env;
 	    module_declarations = md.md_declarations;
 	    module_opened = false;
@@ -161,7 +160,7 @@ let load_module s = function
   | Some f -> let _ = load_module_from true s f in ()
 
 
-(* [require_module] loads and opens a module. *)
+(*s [require_module] loads and opens a module. *)
 
 let require_module spec name fileopt export =
   let file = match fileopt with
@@ -172,7 +171,7 @@ let require_module spec name fileopt export =
   if export then m.module_exported <- true
 
 
-(* [save_module s] saves the module [m] to the disk. *)
+(*s [save_module s] saves the module [m] to the disk. *)
 
 let current_imports () =
   Stringmap.fold
@@ -194,7 +193,7 @@ let save_module_to s f =
   close_out ch
 
 
-(* Pretty-printing of modules state. *)
+(*s Pretty-printing of modules state. *)
 
 let fmt_modules_state () =
   let opened = opened_modules ()