Class Wpalette.toolSource

Configurable palette-tool. Each tool is a widget that consists of three components:

The action button is only displayed when associated with a callback. Clicking the label toggles the configuration panel, if the tool is active.

inherit Frama_c_gui.Widget.widget
method tool : tool

Self cast

method is_active : bool
method on_active : (bool -> unit) -> unit
method set_active : bool -> unit
method has_action : bool
method set_label : string -> unit
method set_status : Frama_c_gui.Widget.icon -> unit
method set_tooltip : string -> unit
method set_action : ?icon:Frama_c_gui.Widget.icon -> ?tooltip:string -> ?callback:(unit -> unit) -> unit -> unit

Makes the action button visible.

  • If no icon is provided, the previous one is kept.
  • If no tooltip is provided, the previous one is kept.
  • If no callback is given, the button is deactivated.
  • The callback replaces any previous one and makes the action button clickable.
method clear_action : unit

Deactivate and hide the action button.

method set_content : Frama_c_gui.Widget.widget -> unit

Shall be used at most once, and before #coerce or #widget.