Module Frama_c_gui.Widget

Simple Widgets

class type widget = object ... end
class type action = object ... end
class type t = widget
class type 'a signal = object ... end
class type 'a selector = object ... end

Labels

type align = [
| `Left
| `Right
| `Center
]
type style = [
| `Label
| `Descr
| `Code
| `Title
]
type color = [
| GDraw.color
| `NORMAL
]
class label : ?style:style -> ?align:align -> ?width:int -> ?text:string -> unit -> object ... end

Default: ~style:`Label ~align:`Left

Icons

type icon = [
| GtkStock.id
| `Share of string
| `None
]
val default_icon : unit -> GdkPixbuf.pixbuf
val shared_icon : string -> GdkPixbuf.pixbuf
val gimage : icon -> GMisc.image
class image : icon -> object ... end

Buttons

class button : ?align:align -> ?icon:icon -> ?label:string -> ?border:bool -> ?tooltip: string -> unit -> object ... end
class toggle : ?align:align -> ?icon:icon -> ?label:string -> ?border:bool -> ?tooltip: string -> unit -> object ... end
class checkbox : label:string -> ?tooltip:string -> unit -> object ... end
class switch : ?tooltip:string -> unit -> object ... end

Groups

class 'a group : 'a -> object ... end

A group is not a widget ; it creates interconnected toggle or radio buttons, each switching to a peculiar value.

Selectors

class spinner : ?min:int -> ?max:int -> ?step:int -> value:int -> ?tooltip:string -> unit -> object ... end
class 'a menu : default:'a -> ?options:('a * string) list -> ?render:( 'a -> string ) -> ?items:'a list -> unit -> object ... end
class popup : unit -> object ... end

Contextual menu. The #popup method can be called inside a right-click callback. For instance: widget#on_right_click menu#popup.