Add support for plugin initialization function

Plugins can call add_known_plugin instead of add_known_module to
specify an initialization function. That function is granted to be
called after the system initialization (in case of static linking)
and every time their are "loaded" with Declare ML Module (even if the
.cmo or .cmxs is actually loaded only once since OCaml is unable to
unload dynamically linked modules).

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

3 files changed, 31 insertions, 3 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 53b3f58933..0fc6d02c1a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -326,6 +326,7 @@ let init arglist =
       if_verbose print_header ();
       init_load_path ();
       inputstate ();
+      Mltop.init_known_plugins ();
       set_vm_opt ();
       engage ();
       if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index ff3ce8a09c..025c972fe9 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -235,9 +235,24 @@ let add_known_module mname =
 let module_is_known mname =
   Stringset.mem (String.capitalize mname) !known_loaded_modules
 
+let known_loaded_plugins = ref Stringmap.empty
+
+let init_ml_object mname =
+  try Stringmap.find mname !known_loaded_plugins ()
+  with Not_found -> ()
+
 let load_ml_object mname fname=
   dir_ml_load fname;
-  add_known_module mname
+  add_known_module mname;
+  init_ml_object mname
+
+let add_known_plugin init name =
+  let name = String.capitalize name in
+  add_known_module name;
+  known_loaded_plugins := Stringmap.add name init !known_loaded_plugins
+
+let init_known_plugins () =
+  Stringmap.iter (fun _ f -> f()) !known_loaded_plugins
 
 (* Summary of declared ML Modules *)
 
@@ -260,7 +275,8 @@ let unfreeze_ml_modules x =
            load_ml_object mname fname
          else
 	   errorlabstrm "Mltop.unfreeze_ml_modules"
-             (str"Loading of ML object file forbidden in a native Coq.");
+             (str"Loading of ML object file forbidden in a native Coq.")
+       else init_ml_object mname;
        add_loaded_module mname)
     x
 
@@ -290,7 +306,8 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 	     raise e
 	 else
 	     (if_verbose msgnl (str" failed]");
-	      error ("Dynamic link not supported (module "^name^")")))
+	      error ("Dynamic link not supported (module "^name^")"))
+       else init_ml_object mname)
     mnames
 
 let classify_ml_module_object ({mlocal=mlocal} as o) =
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 1e9c3b03c7..99b96ed7bd 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -51,6 +51,16 @@ val add_known_module : string -> unit
 val module_is_known : string -> bool
 val load_ml_object : string -> string -> unit
 
+(* 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.
+ * The initialization function is granted to be called after Coq is fully
+ * bootstrapped, even if the plugin is statically linked with the toplevel *)
+val add_known_plugin : (unit -> unit) -> string -> unit
+
+(* Calls all initialization functions in a non-specified order *)
+val init_known_plugins : unit -> unit
+
 (** Summary of Declared ML Modules *)
 val get_loaded_modules : unit -> string list
 val add_loaded_module : string -> unit