module Metrics_gui:sig
..end
val init_panel : Design.main_window_extension_points -> GPack.box
Initialize the main Metrics panel into an upper and lower part.
The panel of Metrics has two parts:
val coerce_panel_to_ui : < coerce : 'a; .. > -> 'b -> string * 'a * 'c option
Returning a value to register in Frama-C's GUI
val display_as_table : string list list -> GPack.box -> unit
Display the list of list of strings in a LablGTK table object
Display the table_contents
matrix as a GTK table
val reset_panel : 'a -> unit
Reset metrics panel to pristine conditions by removing children from bottom container
val register_metrics : ?apply:bool -> string -> (GPack.box -> unit) -> unit
register_metrics metrics_name
display_function
() adds a selectable
choice for the metrics metrics_name
and add a hook calling
display_function
whenever this metrics is selected and launched.
If apply
is true, display_function
is immediately applied. apply
is
false by default.
Add a new metrics to its dedicated panel. The text is added to the combo box while the action is added to the association lists of possible actions.