Module Frama_c_gui.Menu_manager

Handle the menubar and the toolbar.

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

Smart constructors for menu entries.

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

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.