indexing
description: "Control which combines a list box and an edit control."
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-11-14 09:30:31 -0800 (Tue, 14 Nov 2006) $"
revision: "$Revision: 65047 $"
deferred class interface
WEL_COMBO_BOX
feature
commands: WEL_COMMAND_MANAGER
WEL_WINDOW
default_processing: BOOLEAN
WEL_RETURN_VALUE
font: WEL_FONT
WEL_CONTROL
require WEL_CONTROL
exists: exists
ensure WEL_CONTROL
result_not_void: Result /= Void
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
has_return_value: BOOLEAN
WEL_RETURN_VALUE
i_th_text (i: INTEGER_32): STRING_32
`i'
require
exists: exists
i_large_enough: i >= 0
i_small_enough: i < count
ensure
result_exists: Result /= Void
i_th_text_length (i: INTEGER_32): INTEGER_32
`i'
require
exists: exists
i_large_enough: i >= 0
i_small_enough: i < count
ensure
positive_result: Result >= 0
id: INTEGER_32
WEL_CONTROL
item: POINTER
WEL_ANY
message_return_value: POINTER
WEL_RETURN_VALUE
require WEL_RETURN_VALUE
has_return_value: has_return_value
parent: WEL_WINDOW
WEL_WINDOW
feature
count: INTEGER_32
require
exists: exists
ensure
positive_result: Result >= 0
feature
frozen deep_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies (other /= Void and then some.same_type (other))
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
frozen is_deep_equal (other: WEL_COMBO_BOX): BOOLEAN
`Current'`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
shallow_implies_deep: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_deep_equal (Current)
is_equal (other: WEL_COMBO_BOX): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
frozen standard_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: WEL_COMBO_BOX): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
absolute_x: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
Result = window_rect.x
absolute_y: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
Result = window_rect.y
background_brush: WEL_BRUSH
WEL_WINDOW
ensure WEL_WINDOW
new_object: Result /= Void implies Result /= background_brush
captured_window: WEL_WINDOW
WEL_WINDOW
require WEL_WINDOW
exists: exists
window_captured: window_captured
client_rect: WEL_RECT
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
result_not_void: Result /= Void
command (message: INTEGER_32): WEL_COMMAND
`message'
WEL_WINDOW
require WEL_WINDOW
positive_message: message >= 0
command_exists: command_exists (message)
ensure WEL_WINDOW
result_not_void: Result /= Void
command_argument (message: INTEGER_32): ANY
`message'
WEL_WINDOW
require WEL_WINDOW
positive_message: message >= 0
command_exists: command_exists (message)
command_exists (message: INTEGER_32): BOOLEAN
`message'
WEL_WINDOW
require WEL_WINDOW
positive_message: message >= 0
commands_enabled: BOOLEAN
WEL_WINDOW
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
dropped_rect: WEL_RECT
require
exists: exists
ensure
result_not_void: Result /= Void
enabled: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
ex_style: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
exists: BOOLEAN
item
WEL_ANY
ensure WEL_ANY
Result = (item /= default_pointer)
focused_window: WEL_WINDOW
WEL_WINDOW
require WEL_WINDOW
exists: exists
get_text_limit: INTEGER_32
has_capture: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_focus: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_heavy_capture: BOOLEAN
WEL_WINDOW
has_horizontal_scroll_bar: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_system_font: BOOLEAN
WEL_CONTROL
require WEL_CONTROL
exists: exists
has_vertical_scroll_bar: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
heavy_capture_activated: BOOLEAN
has_heavy_capture
WEL_WINDOW
height: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
is_inside: BOOLEAN
WEL_WINDOW
list_item_height: INTEGER_32
ensure
operation_successful: Result /= cb_err
maximal_height: INTEGER_32
WEL_WINDOW
ensure WEL_WINDOW
result_large_enough: Result >= minimal_height
maximal_width: INTEGER_32
WEL_WINDOW
ensure WEL_WINDOW
result_large_enough: Result >= minimal_width
maximized: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
minimal_height: INTEGER_32
WEL_WINDOW
ensure WEL_WINDOW
positive_result: Result >= 0
result_small_enough: Result <= maximal_height
minimal_width: INTEGER_32
WEL_WINDOW
ensure WEL_WINDOW
positive_result: Result >= 0
result_small_enough: Result <= maximal_width
minimized: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
placement: WEL_WINDOW_PLACEMENT
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
result_not_void: Result /= Void
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
selected: BOOLEAN
require
exists: exists
selected_item: INTEGER_32
require
exists: exists
selected: selected
ensure
result_large_enough: Result >= 0
result_small_enough: Result < count
selected_string: STRING_32
require
exists: exists
selected: selected
ensure
result_not_void: Result /= Void
selection_field_height: INTEGER_32
ensure
operation_successful: Result /= cb_err
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
shown: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
style: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
text: STRING_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
result_not_void: Result /= Void
text_length: INTEGER_32
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
positive_result: Result >= 0
top_index: INTEGER_32
ensure
operation_successful: Result /= cb_err
valid_hwnd_constant (c: POINTER): BOOLEAN
`c'
WEL_HWND_CONSTANTS
width: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
window_captured: BOOLEAN
WEL_WINDOW
window_rect: WEL_RECT
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
result_not_void: Result /= Void
x: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
parent = Void implies Result = absolute_x
y: INTEGER_32
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
parent = Void implies Result = absolute_y
feature
disable
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
disabled: not enabled
disable_commands
WEL_WINDOW
ensure WEL_WINDOW
commands_disabled: not commands_enabled
disable_default_processing
WEL_WINDOW
ensure WEL_WINDOW
default_processing_disabled: not default_processing
disable_drag_accept_files
`Current'
WEL_WINDOW
require WEL_WINDOW
exists
enable
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
enabled: enabled
enable_commands
WEL_WINDOW
ensure WEL_WINDOW
commands_enabled: commands_enabled
enable_default_processing
WEL_WINDOW
ensure WEL_WINDOW
default_processing_enabled: default_processing
enable_drag_accept_files
`Current'
WEL_WINDOW
require WEL_WINDOW
exists
hide
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
hidden: not shown
maximize
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
maximized: maximized
minimize
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
minimized: minimized
release_capture
set_capture
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_capture: has_capture
ensure WEL_WINDOW
not_has_capture: not has_capture
release_heavy_capture
set_heavy_capture
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_heavy_capture: has_heavy_capture
heavy_capture_activated: heavy_capture_activated
ensure WEL_WINDOW
heavy_capture_set: not has_heavy_capture
heavy_capture_deactivated: not heavy_capture_activated
restore
minimizemaximize
WEL_WINDOW
require WEL_WINDOW
exists: exists
select_item (index: INTEGER_32)
`index'
require
exists: exists
index_large_enough: index >= 0
index_small_enough: index < count
ensure
selected_item: selected and then selected_item = index
set_capture
`Current'
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_not_capture: not has_capture
has_not_heavy_capture: not has_heavy_capture
ensure WEL_WINDOW
has_capture: has_capture
set_ex_style (an_ex_style: INTEGER_32)
`an_ex_style'ex_style
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_focus
`Current'
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_heavy_capture
`Current'
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_not_heavy_capture: not has_heavy_capture
heavy_capture_deactivated: not heavy_capture_activated
ensure WEL_WINDOW
heavy_capture_set: has_heavy_capture implies heavy_capture_activated
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_style (a_style: INTEGER_32)
style`a_style'
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
show
WEL_WINDOW
require WEL_WINDOW
exists: exists
unselect
require
exists: exists
ensure
selection_cleared: not selected
update_cached_style (new_ex_style, old_ex_style: INTEGER_32)
WEL_WINDOW
feature
add_files (attribut: INTEGER_32; files: STRING_GENERAL)
`files'`files'
`attribut'
require
exists: exists
files_not_void: files /= Void
add_string (a_string: STRING_GENERAL)
`a_string'
require
exists: exists
a_string_not_void: a_string /= Void
ensure
new_count: count = old count + 1
delete_string (index: INTEGER_32)
`index'
require
exists: exists
index_large_enough: index >= 0
index_small_enough: index < count
ensure
new_count: count = old count - 1
disable_redraw
`Current'enable_redraw
WEL_WINDOW
require WEL_WINDOW
exists: exists
enable_redraw
`Current'
WEL_WINDOW
require WEL_WINDOW
exists: exists
has_system_window_locked: BOOLEAN
WEL_WINDOW
insert_string_at (a_string: STRING_GENERAL; index: INTEGER_32)
`a_string'`index'
require
exists: exists
a_string_not_void: a_string /= Void
index_small_enough: index <= count
index_large_enough: index >= 0
ensure
new_count: count = old count + 1
lock_window_update
lock_window_update
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
has_system_window_locked
reset_content
require
exists: exists
ensure
new_count: count = 0
set_font (a_font: WEL_FONT)
font`a_font'
WEL_CONTROL
require WEL_CONTROL
exists: exists
a_font_not_void: a_font /= Void
a_font_exists: a_font.exists
ensure WEL_CONTROL
font_set: not has_system_font implies font.item = a_font.item
set_height (a_height: INTEGER_32)
height`a_height'
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_item (an_item: POINTER)
item`an_item'
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
set_parent (a_parent: WEL_WINDOW)
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_placement (a_placement: WEL_WINDOW_PLACEMENT)
placement`a_placement'
WEL_WINDOW
require WEL_WINDOW
exists: exists
a_placement_not_void: a_placement /= Void
set_text (a_text: STRING_GENERAL)
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
text_set_when_not_void: a_text /= Void