diff options
| -rw-r--r-- | toplevel/mltop.ml | 50 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 23 |
2 files changed, 56 insertions, 17 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 196ab98ed6..11f00d6e54 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 19b9996317..196c0bf94b 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 |