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