diff options
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 23 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 10 |
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 |