Menu_manager (frama-c.Frama_c_gui.Menu

type where =

| Toolbar of GtkStock.id * string * string
(*
Label then tooltip
*)
| Menubar of GtkStock.id option * string
(*
Stock used for icon * Label
*)
| ToolMenubar of GtkStock.id * string * string
(*
Label then tooltip
*)

Where to put a new entry.

since Boron-20100401

type callback_state =

| Unit_callback of unit -> unit
| Bool_callback of bool -> unit * unit -> bool

Callback for the buttons that can be in the menus. Standard buttons/menus have a callback with no argument. Buttons/menus with states are displayed with checkboxes in menus, or as toggle buttons in toolbars. They receive the after-click state as argument. The state of the button with the second argument of Bool_callback. Currently checks menus cannot have images in Gtk, or the GtkStock.id fields of where are ignored.

since Nitrogen-20111001

type entry = private {

e_where : where;
e_callback : callback_state;
(*
callback called when the button is clicked
*)
e_sensitive : unit -> bool;
(*
should the button be activated when the gui is refreshed
*)

}

since Boron-20100401

If not supplied, the sensitive parameter is the function that always returns true.

since Nitrogen-20111001

val toolbar : 
  ?sensitive:(unit -> bool) ->
  icon:GtkStock.id ->
  label:string ->
  ?tooltip:string ->
  callback_state ->
  entry

val menubar : 
  ?sensitive:(unit -> bool) ->
  ?icon:GtkStock.id ->
  string ->
  callback_state ->
  entry

val toolmenubar : 
  ?sensitive:(unit -> bool) ->
  icon:GtkStock.id ->
  label:string ->
  ?tooltip:string ->
  callback_state ->
  entry

class type item = object ... end

The item type corresponding to an entry.

class menu_manager : ?packing:(GObj.widget -> unit) -> Gtk_helper.host -> object ... end

How to handle a Frama-C menu.

Module `Frama_c_gui.Menu_manager`

Smart constructors for menu entries.