Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 94 insertions, 0 deletions

diff --git a/library/library.mli b/library/library.mli
new file mode 100644
index 00000000..18be1671
--- /dev/null
+++ b/library/library.mli
@@ -0,0 +1,94 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+open Util
+open Names
+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]. *)
+
+val read_library : qualid located -> unit
+
+val read_library_from_file : System.physical_path -> unit
+
+(* [import_library true qid] = [export qid] *)
+ 
+val import_library : bool -> qualid located -> unit
+
+val library_is_loaded : dir_path -> bool
+val library_is_opened : dir_path -> bool
+
+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. *)
+
+val library_full_filename : dir_path -> string
+
+
+(*s Global load path *)
+type logical_path = dir_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
+
+exception LibUnmappedDir
+exception LibNotFound
+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. *)
+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