summaryrefslogtreecommitdiff
path: root/library/libobject.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/libobject.mli')
-rw-r--r--library/libobject.mli71
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