class interface HEAD_MENU_ITEM

creation
   make (s: STRING)
      --  Create head menu item.

      require
         valid_string: s /= Void
      ensure
         not_attached: not is_valid

feature(s) from MENU_ITEM
   --  Attributes

   is_valid: BOOLEAN
      --  Is this item valid and attached to a parent menu?


   enabled: BOOLEAN
      --  Is this item enabled or disabled?

      require
         valid: is_valid

   is_checked: BOOLEAN
      --  Does this item have a visible check mark?

      require
         valid: is_valid

feature(s) from MENU_ITEM
   --  Update

   set_name (s: STRING)
      --  Set name. It will not be modified in the actual 
      --  after the parent MENU has been attached.

      require
         valid_string: s /= Void;
         valid_menu: is_valid

   set_help (hs: STRING)
      --  Set the optional help string associated with this item.

      require
         valid_string: hs /= Void

   set_command (gc: GUI_COMMAND)
      --  Optional selection command (if when_selected not redefined).

      require
         nothing:  --  Void means no callback command
      ensure
         keep_reference: command = gc

   set_prepare_command (gc: GUI_COMMAND)
      --  Optional preparation command (if when_prepared not redefined).

      require
         nothing:  --  Void means no callback command
      ensure
         keep_reference: pre_command = gc

   set_leader (lead: HEAD_MENU_ITEM)
      --  Set optional leading menu item for radio-type items.

      require
         valid_lead: lead /= Void;
         not_leader: lead /= Current
      ensure
         keep_reference: lead = leader

feature(s) from MENU_ITEM
   --  Setup

   enable
      --  Enable menu item.

      require
         valid: is_valid
      ensure
         done: enabled

   disable
      --  Grey out menu item.

      require
         valid: is_valid
      ensure
         done: not enabled

   check_mark
      --  Set check mark.

      require
         valid: is_valid
      ensure
         done: is_checked

   uncheck_mark
      --  Unset check mark.

      require
         valid: is_valid
      ensure
         done: not is_checked

   detach
      --  Remove this item from its menu.

      require
         attached: is_valid
      ensure
         detached: not is_valid

feature(s) from MENU_ITEM
   --  Accelerator

   has_accelerator: BOOLEAN
      --  Has this item got an associated keyboard accelerator?


   set_accelerator (newacc: ACCELERATOR)
      --  Set associated keyboard accelerator.

      require
         ok: newacc /= Void
      ensure
         keep_reference: accelerator = newacc;
         done: has_accelerator

feature(s) from MENU_ITEM
   --  Action

   execute
      --  Simulate selection of menu item.



end of HEAD_MENU_ITEM