Module Menu_manager

module Menu_manager: sig .. end

Handle the menubar and the toolbar.


type where = 
| Toolbar of GtkStock.id * string * string (*

Label then tooltip

*)
| Menubar of GtkStock.id option * string (*

Label

*)
| ToolMenubar of GtkStock.id * string * string (*

Label then tooltip

*)

Where to put a new entry.

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.

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

*)
}

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.