class interface STD_DROPDOWN_LISTBOX[G->LISTBOX_ITEM]
creation
   make (p: WINDOW)
      --  Create sorted drop-down list box.
      require
         valid_parent: p /= Void
   make_unsorted (p: WINDOW)
      --  Create unsorted drop-down list box.
      require
         valid: p /= Void
feature(s) from CONTROL
   --  Implementation
   self: CHILD_WINDOW
      --  Associated child window.
feature(s) from CONTROL
   --  Dialog box
   has_dialog_box: BOOLEAN
      --  Check if control has associated dialog box.
   dialog_box: DIALOG
      --  Associated dialog which holds the control.
      require
         has_dialog: has_dialog_box
      ensure
         valid: Result /= Void
feature(s) from CONTROL
   --  Control's font
   set_font (ft: FONT)
      --  Set control font.
      require
         valid_font: ft /= Void
feature(s) from CONTROL
   --  Position, independent
   indep_size: RECTANGLE
      --  Control size using dialog coordinates.
      ensure
         is_copy:  --  can be modified.
   indep_set_size (rect: RECTANGLE)
      --  Set listbox size in independent coordinates.
      --  Note: Control's height is set by the operating system, 
      --  so the height is ignored.
      require
         valid: rect /= Void
      ensure
         height_unchanged:  --  height ignored
         done: rect.is_equal(indep_size)
feature(s) from DIALOG_ELEMENT
   --  Device independent positioning
   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 (item: G)
      --  Add item to the list.
      require
         valid_item: item.is_valid
   remove_all
      --  Reset list.
      ensure
         empty: items.is_empty
feature(s) from LISTBOX
   --  Selection
   has_selection: BOOLEAN
      --  Is an item selected?
   selected_item: G
      --  Currently selected item.
      require
         select_ok: has_selection
   has_item (itm: G): BOOLEAN
      --  Is itm in our list?
   select_item (new: G)
      --  Mark new as selected.
      require
         has: has_item(new)
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
feature(s) from STD_DROPDOWN_LISTBOX
   --  Size.
   set_popup_list_height (h: INTEGER)
      --  Set the height of the popup list
      require
         valid_height: h > 0
   default_size
      --  Set size to default.
invariant
   list_init: items /= Void;
end of STD_DROPDOWN_LISTBOX[G->LISTBOX_ITEM]