deferred class interface MENU feature(s) from MEMORY -- Removal : dispose full_collect -- Force a full collection cycle if garbage collection is -- enabled; do nothing otherwise. feature(s) from MENU -- Menu items management add_popup (item: POPUP_MENU) -- Add a popup menu at the end of the current menu. -- It cannot be removed. require valid_menu: is_valid; valid_item: item /= Void add_separator -- Add a separator at the end of the current menu. -- It cannot be removed. require valid: is_valid add_item (item: MENU_ITEM) -- Add an item at the end of the current menu. -- Use item.detach to remove the item. require valid_menu: is_valid; existing_item: item /= Void; unattached_item: not item.is_valid ensure attached: item.is_valid feature(s) from MENU is_valid: BOOLEAN invariant valid_parent: parent /= Void; items_ok: items /= Void; end of deferred MENU