diff options
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/library/lib.mli b/library/lib.mli index 8981754e..aa874470 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli,v 1.41.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: lib.mli,v 1.41.2.3 2005/01/21 16:41:50 herbelin Exp $ i*) (*i*) open Util @@ -59,7 +59,7 @@ val add_leaf : identifier -> obj -> object_name val add_absolutely_named_leaf : object_name -> obj -> unit val add_anonymous_leaf : obj -> unit -(* this operation adds all objects with the same name and calls load_object +(* this operation adds all objects with the same name and calls [load_object] for each of them *) val add_leaves : identifier -> obj list -> object_name @@ -107,7 +107,7 @@ val start_modtype : module_ident -> module_path -> Summary.frozen -> object_prefix val end_modtype : module_ident -> object_name * object_prefix * Summary.frozen * library_segment -(* Lib.add_frozen_state must be called after each of the above functions *) +(* [Lib.add_frozen_state] must be called after each of the above functions *) (*s Compilation units *) @@ -121,6 +121,9 @@ val library_dp : unit -> dir_path (* Extract the library part of a name even if in a section *) val library_part : global_reference -> dir_path +(* Extract the library part of a name if not in a functor *) +val file_part : global_reference -> dir_path option + (*s Sections *) val open_section : identifier -> object_prefix |