class interface POPUP_MENU creation make (par: OVERLAPPED_WINDOW) -- Create a popup menu, which can be added to a bar or -- to another popup menu. require valid: par /= Void ensure done: is_valid; keep_reference: par = parent 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 feature(s) from POPUP_MENU -- Menu name set_name (s: STRING) -- Set the menu name. It will be used when the menu is -- attached to a another popup menu or a menu bar. require valid_menu: is_valid; valid_string: s /= Void feature(s) from POPUP_MENU -- Installation & Destruction pop_up (p: POINT) -- Display & process popup menu require valid_point: p /= Void destroy -- Destroy the menu. require stand_alone: -- not attached to a window (menu bar) ensure done: not is_valid invariant valid_parent: parent /= Void; items_ok: items /= Void; valid_name: name /= Void; end of POPUP_MENU