module Plugin:sig..end
Plugin registration and general services.
module type S_no_log =sig..end
Special signature for Kernel services, whose messages are handled in an ad'hoc manner.
module type S =sig..end
Provided plug-general services for plug-ins.
type plugin = private {
|
p_name : |
|
p_shortname : |
|
p_help : |
|
p_parameters : |
}
module type General_services =sig..end
module Register:functor (P:sigval name :stringName of the module. Arbitrary non-empty string.
val shortname :stringPrefix for plugin options. No space allowed.
val help :stringdescription of the module. Free-form text.
end) ->General_services
Functors for registering a new plug-in.
: unit -> unitMake visible to the end-user the -<plug-in>-share option.
To be called just before applying Plugin.Register to create plug-in services.
val is_session_visible : unit -> unitMake visible to the end-user the -<plug-in>-session option.
To be called just before applying Plugin.Register to create plug-in services.
val is_config_visible : unit -> unitMake visible to the end-user the -<plug-in>-config option.
To be called just before applying Plugin.Register to create plug-in services.
val plugin_subpath : string -> unitUse the given string as the sub-directory in which the plugin files will
be installed (ie. share/frama-c/plugin_subpath...). Relevant for
directories Share, Session and Config above.
val default_msg_keys : string list -> unitDebug message keys set by default for the plugin.
val get_from_shortname : string -> pluginGet a plug-in from its shortname.
val get_from_name : string -> pluginGet a plug-in from its name.
val is_present : string -> boolWhether a plug-in already exists. Plugins are identified by their short name.
val get : string -> pluginGet a plug-in from its name.
val iter_on_plugins : (plugin -> unit) -> unitIterate on each registered plug-in.
val fold_on_plugins : (plugin -> 'a -> 'a) -> 'a -> 'aFold f on each registered plug-in.