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]