class interface STD_MULTIPLE_LISTBOX[G->LISTBOX_ITEM]
creation
make (p: WINDOW)
-- Create sorted listbox.
require
valid_parent: p /= Void
make_unsorted (p: WINDOW)
-- Create unsorted listbox.
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 (sz: RECTANGLE)
-- Set control size using dialog coordinates.
require
valid: sz /= Void
ensure
done: sz.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 an item to the list.
require
valid_item: item.is_valid
remove_all
-- Remove all items.
ensure
empty: items.is_empty
feature(s) from LISTBOX
-- Selection
has_selection: BOOLEAN
-- Has selection?
selected_item: G
-- Current selected item.
require
select_ok: has_selection
has_item (itm: G): BOOLEAN
-- Is itm in the 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 MULTIPLE_LISTBOX
-- Multiple selection
selected_range: DS_LIST[G]
-- Selected items.
require
select_ok: has_selection
ensure
is_copy: Result /= Void
end of STD_MULTIPLE_LISTBOX[G->LISTBOX_ITEM]