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 = [
  1. | `Left
  2. | `Right
  3. | `Center
]
type style = [
  1. | `Label
  2. | `Descr
  3. | `Code
  4. | `Title
]
type color = [
  1. | GDraw.color
  2. | `NORMAL
]
class label : ?style:style -> ?align:align -> ?width:int -> ?text:string -> unit -> object ... end

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

Icons

type icon = [
  1. | GtkStock.id
  2. | `Share of string
  3. | `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.