Class Menu_manager.menu_manager

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

How to handle a Frama-C menu.


API for plug-ins

method add_plugin : ?title:string -> entry list -> item array

Add entries dedicated to a plug-in. If title is specified, then the entries are added in a dedicated sub-menu of name title. The elements of the returned array are in the same order that the ones in the input list.

method add_debug : ?title:string ->
?show:(unit -> bool) -> entry list -> item array

Add entries to the menu dedicated to debugging tools. If title is specified, then the entries are added in a dedicated sub-menu of name title. If show is specified, then the entries are only shown when this function returns true (it returns true by default). The elements of the returned array are in the same order that the ones in the input list.

High-level API

method add_menu : ?pos:int -> string -> GMenu.menu_item * GMenu.menu
method add_entries : ?title:string ->
?pos:int -> GMenu.menu -> entry list -> item array

Add entries in the given menu. If title is specified, then the entries are added in a dedicated sub-menu of name title. The elements of the returned array are in the same order that the ones in the input list.

method set_sensitive : bool -> unit

Set the sensitive property of all the entries.

Low-level API

method factory : GMenu.menu_shell GMenu.factory
method menubar : GMenu.menu_shell
method toolbar : GButton.toolbar
method refresh : unit -> unit

Reset the activation state of the buttons