deferred class interface MULTIPLE_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
feature(s) from MULTIPLE_LISTBOX
-- Multiple selection
selected_range: DS_LIST[G]
-- Current selected range
require
select_ok: has_selection
ensure
is_copy: Result /= Void
end of deferred MULTIPLE_LISTBOX[G->LISTBOX_ITEM]