diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 43 |
1 files changed, 24 insertions, 19 deletions
diff --git a/library/lib.mli b/library/lib.mli index 686e6a0e2d..30569197bc 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -19,22 +19,24 @@ open Names type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) +val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name + type node = | Leaf of Libobject.obj - | CompilingLibrary of Libnames.object_prefix - | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | OpenedSection of Libnames.object_prefix * Summary.frozen + | CompilingLibrary of Nametab.object_prefix + | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen + | OpenedSection of Nametab.object_prefix * Summary.frozen -type library_segment = (Libnames.object_name * node) list +type library_segment = (Libobject.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list (** {6 Object iteration functions. } *) -val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit -val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit +val open_objects : int -> Nametab.object_prefix -> lib_objects -> unit +val load_objects : int -> Nametab.object_prefix -> lib_objects -> unit val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects -(*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) +(*val load_and_subst_objects : int -> Libnames.Nametab.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*) (** [classify_segment seg] verifies that there are no OpenedThings, clears ClosedSections and FrozenStates and divides Leafs according @@ -46,20 +48,20 @@ val classify_segment : (** [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : - Libnames.object_prefix -> lib_objects -> library_segment + Nametab.object_prefix -> lib_objects -> library_segment (** {6 ... } *) (** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name +val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit -val pull_to_head : Libnames.object_name -> unit +val pull_to_head : Libobject.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name +val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name (** {6 ... } *) @@ -70,7 +72,7 @@ val contents : unit -> library_segment (** The function [contents_after] returns the current library segment, starting from a given section path. *) -val contents_after : Libnames.object_name -> library_segment +val contents_after : Libobject.object_name -> library_segment (** {6 Functions relative to current path } *) @@ -105,28 +107,28 @@ val find_opening_node : Id.t -> node val start_module : export -> module_ident -> ModPath.t -> - Summary.frozen -> Libnames.object_prefix + Summary.frozen -> Nametab.object_prefix val start_modtype : module_ident -> ModPath.t -> - Summary.frozen -> Libnames.object_prefix + Summary.frozen -> Nametab.object_prefix val end_module : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Nametab.object_prefix * Summary.frozen * library_segment val end_modtype : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Nametab.object_prefix * Summary.frozen * library_segment (** {6 Compilation units } *) val start_compilation : DirPath.t -> ModPath.t -> unit -val end_compilation_checks : DirPath.t -> Libnames.object_name +val end_compilation_checks : DirPath.t -> Libobject.object_name val end_compilation : - Libnames.object_name-> Libnames.object_prefix * library_segment + Libobject.object_name-> Nametab.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) @@ -146,9 +148,12 @@ val close_section : unit -> unit type frozen -val freeze : marshallable:Summary.marshallable -> frozen +val freeze : marshallable:bool -> frozen val unfreeze : frozen -> unit +(** Keep only the libobject structure, not the objects themselves *) +val drop_objects : frozen -> frozen + val init : unit -> unit (** {6 Section management for discharge } *) |