module Library

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

1 files changed, 28 insertions, 28 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index f5e610704..1096ac43a 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -5,15 +5,17 @@ open Util
 open Names
 
 type 'a object_declaration = {
-  load_function : 'a -> unit;
   cache_function : section_path * 'a -> unit;
+  load_function : 'a -> unit;
+  open_function : 'a -> unit;
   specification_function : 'a -> 'a }
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
 type dynamic_object_declaration = {
-  dyn_load_function : obj -> unit;
   dyn_cache_function : section_path * obj -> unit;
+  dyn_load_function : obj -> unit;
+  dyn_open_function : obj -> unit;
   dyn_specification_function : obj -> obj }
 
 let object_tag lobj = Dyn.tag lobj
@@ -23,41 +25,39 @@ let cache_tab =
 
 let declare_object (na,odecl) =
   let (infun,outfun) = Dyn.create na in
-  let loader lobj =
-    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the loadfun"
-  and cacher (spopt,lobj) =
+  let cacher (spopt,lobj) =
     if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the cachefun"
+  and loader lobj =
+    if Dyn.tag lobj = na then odecl.load_function (outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the loadfun"
+  and opener lobj =
+    if Dyn.tag lobj = na then odecl.open_function (outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the openfun"
   and spec_extractor lobj = 
     infun(odecl.specification_function (outfun lobj))
   in 
-  Hashtbl.add cache_tab na { dyn_load_function = loader;
-                             dyn_cache_function = cacher;
+  Hashtbl.add cache_tab na { dyn_cache_function = cacher;
+			     dyn_load_function = loader;
+                             dyn_open_function = opener;
                              dyn_specification_function = spec_extractor };
   (infun,outfun)
 
-
-let load_object lobj =
+let apply_dyn_fun f lobj =
   let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in 
-    dodecl.dyn_load_function lobj
-  with Not_found ->
-    anomaly ("Cannot find loadfun for an object with tag "^tag)
+  try
+    let dodecl = Hashtbl.find cache_tab tag in f dodecl
+  with Not_found -> 
+    anomaly ("Cannot find library functions for an object with tag "^tag)
 
-let cache_object (spopt,lobj) =
-  let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in 
-    dodecl.dyn_cache_function(spopt,lobj)
-  with Not_found ->
-    anomaly ("Cannot find cachefun for an object with tag "^tag)
+let cache_object ((_,lobj) as node) =
+  apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
+
+let load_object lobj = 
+  apply_dyn_fun (fun d -> d.dyn_load_function lobj) lobj
+
+let open_object lobj = 
+  apply_dyn_fun (fun d -> d.dyn_open_function lobj) lobj
 
 let extract_object_specification lobj =
-  let tag = object_tag lobj in
-  try 
-    let dodecl = Hashtbl.find cache_tab tag in
-    dodecl.dyn_specification_function lobj
-  with Not_found ->
-    anomaly ("Cannot find specification extractor for an object with tag "^tag)
+  apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj