module_segment et module_filename

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

3 files changed, 33 insertions, 21 deletions

diff --git a/library/lib.mli b/library/lib.mli
index 1d601f7b6..cf8b173b0 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -7,7 +7,7 @@ open Libobject
 open Summary
 (*i*)
 
-(* This module provides a general mechanism to keep a trace of all operations
+(*s This module provides a general mechanism to keep a trace of all operations
    and to backtrack (undo) those operations. It provides also the section
    mechanism (at a low level; discharge is not known at this step). *)
 
@@ -29,6 +29,11 @@ and library_segment = library_entry list
 val add_leaf : identifier -> path_kind -> obj -> section_path
 val add_anonymous_leaf : obj -> unit
 
+
+(*s The function [contents_after] returns the current library segment, 
+    starting from a given section path. If not given, the entire segment
+    is returned. *)
+
 val contents_after : section_path option -> library_segment
 
 
diff --git a/library/library.ml b/library/library.ml
index 3bd19dc1a..d3af39071 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 ()
diff --git a/library/library.mli b/library/library.mli
index 0eb47bd3a..474669452 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,7 +1,7 @@
 
 (* $Id$ *)
 
-(* This module is the heart of the library. It provides low level functions to
+(*s This module is the heart of the library. It provides low level functions to
    load, open and save modules. Modules are saved onto the disk with checksums
    (obtained with the [Digest] module), which are checked at loading time to
    prevent inconsistencies between files written at various dates. It also
@@ -32,6 +32,14 @@ val require_module : bool option -> string -> string option -> bool -> unit
 
 val save_module_to : string -> string -> unit
 
+(*s [module_segment m] returns the segment of the loaded module
+    [m]; if not given, the segment of the current module is returned
+    (which is then the same as [Lib.contents_after None]). 
+    [module_filename] returns the full filename of a loaded module. *)
+
+val module_segment : string option -> Lib.library_segment
+val module_filename : string -> string
+
 (*s Global load path *)
 val get_load_path : unit -> string list
 val add_path : string -> unit