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
Holds the selected filename, "" by default.
""
method set_tooltip : (string -> string) -> unit
Set the pretty-printer for tooltip.
method set_display : (string -> string) -> unit
Set the pretty-printer for button.