Menu_manager.menu_managerSourceHow to handle a Frama-C menu.
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.
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.
method add_entries : ?title:string ->
?pos:int ->
GMenu.menu ->
entry list ->
item arrayAdd 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 factory : GMenu.menu_shell GMenu.factorymethod toolbar : GButton.toolbar