Module Frama_c_gui.WpaneSource

Panels

Form

Sourcetype field = [
  1. | `Compact
    (*

    Fixed size. Does not expand.

    *)
  2. | `Field
    (*

    Single line field. Expands to the left.

    *)
  3. | `Panel
    (*

    Multiline field. Expands to both left and bottom.

    *)
]

The expansible attribute of a field.

A form with various field types.

The form consists of two columns, with one entry per line. Left columns is reserved for (optional) labels. Fields take place in right column. It is also possible to add widget that spans over the two columns.

The form can be horizontally divided into sections.

Elements must be added in left-to-right, top-down order.

Sourceclass form : unit -> object ... end

Tabbed-pane

Sourceclass 'a notebook : ?tabs:Gtk.Tags.position -> default:'a -> unit -> object ... end

Array of Widgets

Sourceclass type entry = object ... end
Sourceclass 'a warray : ?dir:Gtk.Tags.orientation -> ?entry:('a -> entry) -> unit -> object ... end

Dialogs

Sourcetype 'a action = [
  1. | `CANCEL
    (*

    Cancel choice (same as closing the dialog or `MAIN `CANCEL)

    *)
  2. | `APPLY
    (*

    Default choice (same as `DEFAULT `APPLY)

    *)
  3. | `DEFAULT of 'a
    (*

    Default choice (right, small, default button)

    *)
  4. | `SELECT of 'a
    (*

    Secondary choice (right, small button)

    *)
  5. | `ALT of 'a
    (*

    Alternative choice (left, large button)

    *)
  6. | `ACTION of unit -> unit
    (*

    Button (left, large button)

    *)
]

Button for dialog options

Dialog Window.

Dialog window are asynchronous and modal. To open the dialog, invoke run. The method returns immediately. When running, the main window is no more sensitive (dialog is modal). When an action-button is pressed, or the method select is invoked, the associated signal is emitted, and the dialog is dismissed. Then focus goes back to the main window, and the dialog can be re-emitted.

Sourceclass 'a dialog : title:string -> window:GWindow.window -> ?resize:bool -> unit -> object ... end