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, 8 insertions, 16 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 381b67726..bdc6ab89d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -65,17 +65,10 @@ module MakeTable =
 
     module MySet = Set.Make (struct type t = A.t let compare = compare end)
 
-    let t = ref (MySet.empty : MySet.t)
-
-    let _ =
-      if A.synchronous then
-	let freeze () = !t in
-	let unfreeze c = t := c in
-	let init () = t := MySet.empty in
-	Summary.declare_summary nick
-          { Summary.freeze_function = freeze;
-            Summary.unfreeze_function = unfreeze;
-            Summary.init_function = init }
+    let t =
+      if A.synchronous
+      then Summary.ref MySet.empty ~name:nick
+      else ref MySet.empty
 
     let (add_option,remove_option) =
       if A.synchronous then
@@ -216,7 +209,6 @@ with Not_found ->
     or List.mem_assoc (nickname key) !ref_table
   then error "Sorry, this option name is already used."
 
-open Summary
 open Libobject
 open Lib
 
@@ -247,10 +239,10 @@ let declare_option cast uncast
 		       discharge_function = (fun (_,v) -> Some v);
 		       load_function = (fun _ (_,v) -> write v)}
     in
-    let _ = declare_summary (nickname key)
-	     { freeze_function = read;
-	       unfreeze_function = write;
-	       init_function = (fun () -> write default) }
+    let _ = Summary.declare_summary (nickname key)
+	     { Summary.freeze_function = read;
+	       Summary.unfreeze_function = write;
+	       Summary.init_function = (fun () -> write default) }
     in
     begin fun v -> add_anonymous_leaf (decl_obj v) end ,
     begin fun v -> add_anonymous_leaf (ldecl_obj v) end ,