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