code simplifications concerning Summary

 - Most of the time, the table registered via Summary.declare_summary
   is just a single reference. A new function Summary.ref now allows
   to both declare this ref and register it to summary in one shot.

 - Clarifications concerning the role of [init_function].
   For statically registered tables that don't need a special initializer,
   just do nothing there (see the new Summary.nop function).

 Beware: now that Summary exports a function named "ref", any code that
 do an "open Summary" will probably fail to compile.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 7 deletions

diff --git a/library/summary.mli b/library/summary.mli
index 7ded099ab..fd1b324c9 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -14,17 +14,36 @@ type 'a summary_declaration = {
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
+(** For tables registered during the launch of coqtop, the [init_function]
+    will be run only once, during an [init_summaries] done at the end of
+    coqtop initialization. For tables registered later (for instance
+    during a plugin dynlink), [init_function] is used when unfreezing
+    an earlier frozen state that doesn't contain any value for this table.
+
+    Beware: for tables registered dynamically after the initialization
+    of Coq, their init functions may not be run immediately. It is hence
+    the responsability of plugins to initialize themselves properly.
+*)
+
 val declare_summary : string -> 'a summary_declaration -> unit
 
+(** All-in-one reference declaration + summary registration.
+    It behaves just as OCaml's standard [ref] function, except
+    that a [declare_summary] is done, with [name] as string.
+    The [init_function] restores the reference to its initial value. *)
+
+val ref : name:string -> 'a -> 'a ref
+
+(** For global tables registered statically before the end of coqtop
+    launch, the following empty [init_function] could be used. *)
+
+val nop : unit -> unit
+
+(** The type [frozen] is a snapshot of the states of all the registered
+    tables of the system. *)
+
 type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit
-
-(** Beware: if some code is dynamically loaded via dynlink after the
-    initialization of Coq, the init functions of any summary declared
-    by this code may not be run. It is hence the responsability of
-    plugins to initialize themselves properly.
-*)
-