diff options
Diffstat (limited to 'library/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 71 |
1 files changed, 31 insertions, 40 deletions
diff --git a/library/libobject.mli b/library/libobject.mli index 4ec5746b..9c0abafd 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Names @@ -18,38 +18,38 @@ open Mod_subst * a caching function specifying how to add the object in the current scope; - If the object wishes to register its visibility in the Nametab, + If the object wishes to register its visibility in the Nametab, it should do so for all possible sufixes. - * a loading function, specifying what to do when the module - containing the object is loaded; - If the object wishes to register its visibility in the Nametab, - it should do so for all sufixes no shorter then the "int" argument + * a loading function, specifying what to do when the module + containing the object is loaded; + If the object wishes to register its visibility in the Nametab, + it should do so for all sufixes no shorter than the "int" argument - * an opening function, specifying what to do when the module + * an opening function, specifying what to do when the module containing the object is opened (imported); - If the object wishes to register its visibility in the Nametab, - it should do so for the sufix of the length the "int" argument + If the object wishes to register its visibility in the Nametab, + it should do so for the suffix of the length the "int" argument - * a classification function, specyfying what to do with the object, + * a classification function, specifying what to do with the object, when the current module (containing the object) is ended; The possibilities are: - Dispose - the object dies at the end of the module - Substitue - meaning the object is substitutive and - the module name must be updated - Keep - the object is not substitutive, but survives module - closing - Anticipate - this is for objects which have to be explicitely - managed by the [end_module] function (like Require - and Read markers) + Dispose - the object dies at the end of the module + Substitute - meaning the object is substitutive and + the module name must be updated + Keep - the object is not substitutive, but survives module + closing + Anticipate - this is for objects that have to be explicitely + managed by the [end_module] function (like Require + and Read markers) The classification function is also an occasion for a cleanup - (if this function returns Keep or Substitute of some object, the + (if this function returns Keep or Substitute of some object, the cache method is never called for it) - * a substitution function, performing the substitution; - this function should be declared for substitutive objects - only (see obove) + * a substitution function, performing the substitution; + this function should be declared for substitutive objects + only (see above) * a discharge function, that is applied at section closing time to collect the data necessary to rebuild the discharged form of the @@ -59,16 +59,9 @@ open Mod_subst rebuild the non volatile content of a section from the data collected by the discharge function - * an export function, to enable optional writing of its contents - to disk (.vo). This function is also the oportunity to remove - redundant information in order to keep .vo size small - - The export function is a little obsolete and will be removed - in the near future... - *) -type 'a substitutivity = +type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a type 'a object_declaration = { @@ -76,13 +69,12 @@ type 'a object_declaration = { cache_function : object_name * 'a -> unit; load_function : int -> object_name * 'a -> unit; open_function : int -> object_name * 'a -> unit; - classify_function : object_name * 'a -> 'a substitutivity; - subst_function : object_name * substitution * 'a -> 'a; + classify_function : 'a -> 'a substitutivity; + subst_function : substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : 'a -> 'a; - export_function : 'a -> 'a option } + rebuild_function : 'a -> 'a } -(* The default object is a "Keep" object with empty methods. +(* The default object is a "Keep" object with empty methods. Object creators are advised to use the construction [{(default_object "MY_OBJECT") with cache_function = ... @@ -94,7 +86,7 @@ type 'a object_declaration = { val default_object : string -> 'a object_declaration (* the identity substitution function *) -val ident_subst_function : object_name * substitution * 'a -> 'a +val ident_subst_function : substitution * 'a -> 'a (*s Given an object declaration, the function [declare_object] will hand back two functions, the "injection" and "projection" @@ -102,7 +94,7 @@ val ident_subst_function : object_name * substitution * 'a -> 'a type obj -val declare_object : +val declare_object : 'a object_declaration -> ('a -> obj) * (obj -> 'a) val object_tag : obj -> string @@ -110,9 +102,8 @@ val object_tag : obj -> string val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit val open_object : int -> object_name * obj -> unit -val subst_object : object_name * substitution * obj -> obj -val classify_object : object_name * obj -> obj substitutivity -val export_object : obj -> obj option +val subst_object : substitution * obj -> obj +val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj val relax : bool -> unit |