deferred class interface LISTBOX[G->LISTBOX_ITEM]

feature(s) from DIALOG_ELEMENT
   --  Parent

   has_dialog_box: BOOLEAN
      --  Does the object has a valid corresponding dialog?


   dialog_box: DIALOG
      --  The object which uses dialog elements.

      require
         has_dialog: has_dialog_box
      ensure
         valid: Result /= Void

feature(s) from DIALOG_ELEMENT
   --  Device independent positioning

   indep_size: RECTANGLE
      --  Size of element using device independent coordinates.

      ensure
         is_copy:  --  can be modified.

   indep_set_size (r: RECTANGLE)
      --  Set element's size in device independent coordinates.

      require
         valid: r /= Void
      ensure
         done: r.is_equal(indep_size)

   indep_set_point (p: POINT)
      --  Set upper-left point of element using device independent units.

      require
         valid_point: p /= Void

   indep_set_width (wi: INTEGER)
      --  Set element's width using device independent units.

      require
         valid: wi >= 0

   indep_set_height (he: INTEGER)
      --  Set element's height using device independent units.

      require
         valid: he >= 0

feature(s) from DIALOG_ELEMENT
   --  Relative positioning

   place_right (other: DIALOG_ELEMENT)
      --  Place the current element to the right of other.

      require
         valid_other: other /= Void

   place_left (other: DIALOG_ELEMENT)
      --  Place the current element to the left of other.

      require
         valid_other: other /= Void

   place_above (other: DIALOG_ELEMENT)
      --  Place the current element above other.

      require
         valid_other: other /= Void

   place_under (other: DIALOG_ELEMENT)
      --  Place the current element under other.

      require
         valid_other: other /= Void

   place_just_under (other: DIALOG_ELEMENT)
      --  Place the current element exactly under 'other'.


   same_width (other: DIALOG_ELEMENT)
      --  Set the current element width to other's.

      require
         valid_other: other /= Void

   same_height (other: DIALOG_ELEMENT)
      --  Set the current element height to be the same as other's.

      require
         valid_other: other /= Void

   align_left (other: DIALOG_ELEMENT)
      --  Align left side of this element with the 
      --  left side of other.

      require
         ok: other /= Void

   align_right (other: DIALOG_ELEMENT)
      --  Align the right side of this element with the right 
      --  side of other.

      require
         ok: other /= Void

   align_top (other: DIALOG_ELEMENT)
      --  Align the top of this element with top of other.

      require
         ok: other /= Void

   align_bottom (other: DIALOG_ELEMENT)
      --  Align the bottom of this element with bottom of other.

      require
         ok: other /= Void

feature(s) from LISTBOX
   --  Manage associated list

   add_list (lst: DS_LINEAR[G])
      --  Add items to the list box.

      require
         valid_list: lst /= Void

   add_item (x: G)
      --  Add a single item to the list box.

      require
         valid_item: x.is_valid

   remove_all
      --  Remove all items.


feature(s) from LISTBOX
   --  Selection

   has_selection: BOOLEAN
      --  Is (at least) one item selected?


   selected_item: G
      --  Current selected item.

      require
         select_ok: has_selection

   has_item (i: G): BOOLEAN
      --  Is item an item of this list?


   select_item (newitem: G)
      --  Select item.

      require
         has: has_item(newitem)

feature(s) from LISTBOX
   --  Commands

   set_select_command (gc: GUI_COMMAND)
      --  Set when_selected command.

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

   set_execute_command (gc: GUI_COMMAND)
      --  Set when_execute command.

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


end of deferred LISTBOX[G->LISTBOX_ITEM]