Module Metrics_gui.Metrics_gui_panelsSource

GUI utilities for Metrics

Initialize the main Metrics panel into an upper and lower part.

  • returns

    a box containing the lower part of the panel where metrics can display their results.

Sourceval coerce_panel_to_ui : < coerce : 'a.. > -> 'b -> string * 'a * 'c option
  • returns

    a value allowing to register the panel into the main GUI

Sourceval display_as_table : string list list -> GPack.box -> unit

Display the list of list of strings in a LablGTK table object

Sourceval reset_panel : 'a -> unit

Reset metrics panel to pristine conditions by removing children from bottom container

Sourceval 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.