Wfile.button
A button associated with a dialog to select the file.
inherit Frama_c_gui.Widget.widget
inherit dialog
inherit string Frama_c_gui.Widget.selector
method set_tooltip : ( string -> string ) -> unit
Set the pretty-printer for tooltip.
method set_display : ( string -> string ) -> unit
Set the pretty-printer for button.