diff options
-rw-r--r-- | library/lib.mli | 7 | ||||
-rw-r--r-- | library/library.ml | 37 | ||||
-rw-r--r-- | library/library.mli | 10 |
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 |