Wpalette.tool
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 set_status : Frama_c_gui.Widget.icon -> unit
method set_action : ?icon:Frama_c_gui.Widget.icon ->
?tooltip:string ->
?callback:( unit -> unit ) ->
unit ->
unit
Makes the action button visible.
method set_content : Frama_c_gui.Widget.widget -> unit
Shall be used at most once, and before #coerce
or #widget
.