Adding the possibility for ML modules to declare functions to be called at

caching time, i.e. when the Declare ML Module command is evaluated. This can
be used by both static and dynamic plugins.

2 files changed, 56 insertions, 17 deletions

diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 196ab98ed..11f00d6e5 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -264,6 +264,21 @@ let add_known_plugin init name =
 let init_known_plugins () =
   String.Map.iter (fun _ f -> f()) !known_loaded_plugins
 
+(** Registering functions to be used at caching time, that is when the Declare
+    ML module command is issued. *)
+
+let cache_objs = ref String.Map.empty
+
+let declare_cache_obj f name =
+  let objs = try String.Map.find name !cache_objs with Not_found -> [] in
+  let objs = f :: objs in
+  cache_objs := String.Map.add name objs !cache_objs
+
+let perform_cache_obj name =
+  let objs = try String.Map.find name !cache_objs with Not_found -> [] in
+  let objs = List.rev objs in
+  List.iter (fun f -> f ()) objs
+
 (** ml object = ml module or plugin *)
 
 let init_ml_object mname =
@@ -299,21 +314,23 @@ let if_verbose_load verb f name fname =
     or simulate its reload (i.e. doing nothing except maybe
     an initialization function). *)
 
-let cache_ml_object verb reinit name =
-  begin
-    if module_is_known name then
-      (if reinit then init_ml_object name)
-    else if not has_dynlink then
-      error ("Dynamic link not supported (module "^name^")")
-    else
-      if_verbose_load (verb && is_verbose ())
-	load_ml_object name (file_of_name name)
-  end;
-  add_loaded_module name
+let trigger_ml_object verb cache reinit name =
+  if module_is_known name then begin
+    if reinit then init_ml_object name;
+    add_loaded_module name;
+    if cache then perform_cache_obj name
+  end else if not has_dynlink then
+    error ("Dynamic link not supported (module "^name^")")
+  else begin
+    let file = file_of_name name in
+    if_verbose_load (verb && is_verbose ()) load_ml_object name file;
+    add_loaded_module name;
+    if cache then perform_cache_obj name
+  end
 
 let unfreeze_ml_modules x =
   reset_loaded_modules ();
-  List.iter (cache_ml_object false false) x
+  List.iter (trigger_ml_object false false false) x
 
 let _ =
   Summary.declare_summary Summary.ml_modules
@@ -329,7 +346,12 @@ type ml_module_object = {
 }
 
 let cache_ml_objects (_,{mnames=mnames}) =
-  List.iter (cache_ml_object true true) mnames
+  let iter obj = trigger_ml_object true true true obj in
+  List.iter iter mnames
+
+let load_ml_objects _ (_,{mnames=mnames}) =
+  let iter obj = trigger_ml_object true false true obj in
+  List.iter iter mnames
 
 let classify_ml_objects ({mlocal=mlocal} as o) =
   if mlocal then Dispose else Substitute o
@@ -337,8 +359,8 @@ let classify_ml_objects ({mlocal=mlocal} as o) =
 let inMLModule : ml_module_object -> obj =
   declare_object
     {(default_object "ML-MODULE") with
-      load_function = (fun _ -> cache_ml_objects);
       cache_function = cache_ml_objects;
+      load_function = load_ml_objects;
       subst_function = (fun (_,o) -> o);
       classify_function = classify_ml_objects }
 
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 19b999631..196c0bf94 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** {5 Toplevel management} *)
+
 (** If there is a toplevel under Coq, it is described by the following
    record. *)
 type toplevel = {
@@ -26,12 +28,14 @@ val remove : unit -> unit
 (** Tests if an Ocaml toplevel runs under Coq *)
 val is_ocaml_top : unit -> bool
 
-(** Tests if we can load ML files *)
-val has_dynlink : bool
-
 (** Starts the Ocaml toplevel loop *)
 val ocaml_toploop : unit -> unit
 
+(** {5 ML Dynlink} *)
+
+(** Tests if we can load ML files *)
+val has_dynlink : bool
+
 (** Dynamic loading of .cmo *)
 val dir_ml_load : string -> unit
 
@@ -51,6 +55,8 @@ val add_known_module : string -> unit
 val module_is_known : string -> bool
 val load_ml_object : string -> string -> unit
 
+(** {5 Initialization functions} *)
+
 (** Declare a plugin and its initialization function.
     A plugin is just an ML module with an initialization function.
     Adding a known plugin implies adding it as a known ML module.
@@ -61,8 +67,19 @@ val add_known_plugin : (unit -> unit) -> string -> unit
 (** Calls all initialization functions in a non-specified order *)
 val init_known_plugins : unit -> unit
 
+(** Register a callback that will be called when the module is declared with
+    the Declare ML Module command. This is useful to define Coq objects at that
+    time only. Several functions can be defined for one module; they will be
+    called in the order of declaration, and after the ML module has been
+    properly initialized. *)
+val declare_cache_obj : (unit -> unit) -> string -> unit
+
+(** {5 Declaring modules} *)
+
 val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
 
+(** {5 Utilities} *)
+
 val print_ml_path : unit -> Pp.std_ppcmds
 val print_ml_modules : unit -> Pp.std_ppcmds
 val print_gc : unit -> Pp.std_ppcmds