module Metrics_gui:sig
..end
table_contents
matrix as a GTK table
type ('a, 'b, 'c)
metrics_panel = {
|
top : |
|
bottom : |
|
actions : |
val display_as_table : string list list -> GPack.box -> unit
table_contents
matrix as a GTK table
Diplay the list of list of strings in a LablgGTK table object
val clear_container : < children : < destroy : unit -> unit; .. > list; .. > -> unit
val init_panel : unit -> GPack.box
Initialize the main Metrics panel into an upper and lower part.
val reset_panel : 'a -> unit
val coerce_panel_to_ui : < coerce : 'a; .. > -> 'b -> string * 'a * 'c option
val register_metrics : 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.