From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- library/library.mli | 94 ++++++++++++++++++++++------------------------------- 1 file changed, 39 insertions(+), 55 deletions(-) (limited to 'library/library.mli') diff --git a/library/library.mli b/library/library.mli index 18be1671..f7620682 100644 --- a/library/library.mli +++ b/library/library.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: library.mli,v 1.23.2.1 2004/07/16 19:30:36 herbelin Exp $ i*) +(*i $Id: library.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) (*i*) open Util @@ -15,65 +15,58 @@ open Libnames open Libobject (*i*) -(*s This module is the heart of the library. It provides low level - functions to load, open and save libraries. Libraries 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 provides a high - level function [require] which corresponds to the vernacular - command [Require]. *) +(*s This module provides functions to load, open and save + libraries. Libraries correspond to the subclass of modules that + coincide with a file on disk (the ".vo" files). Libraries on the + disk comes with checksums (obtained with the [Digest] module), which + are checked at loading time to prevent inconsistencies between files + written at various dates. +*) + +(*s Require = load in the environment + open (if the optional boolean + is not [None]); mark also for export if the boolean is [Some true] *) +val require_library : qualid located list -> bool option -> unit +val require_library_from_file : + identifier option -> System.physical_path -> bool option -> unit + +(*s Open a module (or a library); if the boolean is true then it's also + an export otherwise just a simple import *) +val import_module : bool -> qualid located -> unit -val read_library : qualid located -> unit +(*s Start the compilation of a library *) +val start_library : string -> dir_path * string -val read_library_from_file : System.physical_path -> unit +(*s End the compilation of a library and save it to a ".vo" file *) +val save_library_to : dir_path -> string -> unit -(* [import_library true qid] = [export qid] *) - -val import_library : bool -> qualid located -> unit +(*s Interrogate the status of libraries *) + (* - Tell if a library is loaded or opened *) val library_is_loaded : dir_path -> bool val library_is_opened : dir_path -> bool + (* - Tell which libraries are loaded or imported *) val loaded_libraries : unit -> dir_path list val opened_libraries : unit -> dir_path list -val fmt_libraries_state : unit -> Pp.std_ppcmds - -(*s Require. The command [require_library spec m file export] loads and opens - a library [m]. [file] specifies the filename, if not [None]. [spec] - specifies to look for a specification ([true]) or for an implementation - ([false]), if not [None]. And [export] specifies if the library must be - exported. *) - -val require_library : - bool option -> qualid located list -> bool -> unit - -val require_library_from_file : - bool option -> identifier option -> System.physical_path -> bool -> unit - -val set_xml_require : (dir_path -> unit) -> unit - -(*s [save_library_to s f] saves the current environment as a library [s] - in the file [f]. *) - -val start_library : string -> dir_path * string -val save_library_to : dir_path -> string -> unit - -(* [library_full_filename] returns the full filename of a loaded library. *) - + (* - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string +(*s Hook for the xml exportation of libraries *) +val set_xml_require : (dir_path -> unit) -> unit -(*s Global load path *) -type logical_path = dir_path +(*s Global load paths: a load path is a physical path in the file + system; to each load path is associated a Coq [dir_path] (the "logical" + path of the physical path) *) -val get_load_path : unit -> System.physical_path list -val get_full_load_path : unit -> (System.physical_path * logical_path) list -val add_load_path_entry : System.physical_path * logical_path -> unit -val remove_path : System.physical_path -> unit -val find_logical_path : System.physical_path -> logical_path -val load_path_of_logical_path : dir_path -> System.physical_path list +val get_load_paths : unit -> System.physical_path list +val get_full_load_paths : unit -> (System.physical_path * dir_path) list +val add_load_path : System.physical_path * dir_path -> unit +val remove_load_path : System.physical_path -> unit +val find_logical_path : System.physical_path -> dir_path +val load_paths_of_dir_path : dir_path -> System.physical_path list +(*s Locate a library in the load paths *) exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath @@ -81,14 +74,5 @@ type library_location = LibLoaded | LibInPath val locate_qualified_library : qualid -> library_location * dir_path * System.physical_path - -val check_required_library : string list -> unit - -(*s Displays the memory use of a library. *) +(*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds - -(* For discharge *) -type library_reference - -val out_require : Libobject.obj -> library_reference -val reload_library : library_reference -> unit -- cgit v1.2.3