indexing
description: "This control permits the user to enter and edit text from the keyboard. Ancestor of WEL_SINGLE_LINE_EDIT and WEL_MULTIPLE_LINE_EDIT."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
deferred class interface
WEL_EDIT
feature
background_color: WEL_COLOR_REF
require WEL_COLOR_CONTROL
exists: exists
ensure WEL_COLOR_CONTROL
color_not_void: background_color /= void
Color_activeborder: INTEGER is 10
WEL_COLOR_CONSTANTS
Color_activecaption: INTEGER is 2
WEL_COLOR_CONSTANTS
Color_appworkspace: INTEGER is 12
WEL_COLOR_CONSTANTS
Color_background: INTEGER is 1
WEL_COLOR_CONSTANTS
Color_btnface: INTEGER is 15
WEL_COLOR_CONSTANTS
Color_btnhighlight: INTEGER is 20
WEL_COLOR_CONSTANTS
Color_btnshadow: INTEGER is 16
WEL_COLOR_CONSTANTS
Color_btntext: INTEGER is 18
WEL_COLOR_CONSTANTS
Color_captiontext: INTEGER is 9
WEL_COLOR_CONSTANTS
Color_graytext: INTEGER is 17
WEL_COLOR_CONSTANTS
Color_highlight: INTEGER is 13
WEL_COLOR_CONSTANTS
Color_highlighttext: INTEGER is 14
WEL_COLOR_CONSTANTS
Color_inactiveborder: INTEGER is 11
WEL_COLOR_CONSTANTS
Color_inactivecaption: INTEGER is 3
WEL_COLOR_CONSTANTS
Color_inactivecaptiontext: INTEGER is 19
WEL_COLOR_CONSTANTS
Color_menu: INTEGER is 4
WEL_COLOR_CONSTANTS
Color_menutext: INTEGER is 7
WEL_COLOR_CONSTANTS
Color_scrollbar: INTEGER is 0
WEL_COLOR_CONSTANTS
Color_window: INTEGER is 5
WEL_COLOR_CONSTANTS
Color_windowframe: INTEGER is 6
WEL_COLOR_CONSTANTS
Color_windowtext: INTEGER is 8
WEL_COLOR_CONSTANTS
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
foreground_color: WEL_COLOR_REF
WEL_STATIC
require WEL_COLOR_CONTROL
exists: exists
ensure WEL_COLOR_CONTROL
color_not_void: foreground_color /= void
has_return_value: BOOLEAN
WEL_RETURN_VALUE
id: INTEGER
WEL_CONTROL
item: POINTER
WEL_ANY
message_return_value: INTEGER
WEL_RETURN_VALUE
require WEL_RETURN_VALUE
has_return_value: has_return_value
parent: WEL_WINDOW
WEL_WINDOW
feature
absolute_x: INTEGER
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
Result = window_rect.x
absolute_y: INTEGER
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
can_undo: BOOLEAN
require
exists: exists
captured_window: WEL_WINDOW
WEL_WINDOW
require WEL_WINDOW
exists: exists
window_captured: window_captured
caret_position: INTEGER
require
exists: exists
client_rect: WEL_RECT
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
result_not_void: Result /= void
command (message: INTEGER): 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): ANY
message
WEL_WINDOW
require WEL_WINDOW
positive_message: message >= 0
command_exists: command_exists (message)
command_exists (message: INTEGER): BOOLEAN
message
WEL_WINDOW
require WEL_WINDOW
positive_message: message >= 0
commands_enabled: BOOLEAN
WEL_WINDOW
enabled: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
ex_style: INTEGER
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
formatting_rect: WEL_RECT
require
exists: exists
ensure
result_not_void: Result /= void
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_selection: BOOLEAN
require
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
WEL_WINDOW
require WEL_WINDOW
exists: exists
is_inside: BOOLEAN
WEL_WINDOW
maximal_height: INTEGER
WEL_WINDOW
ensure WEL_WINDOW
result_large_enough: Result >= minimal_height
maximal_width: INTEGER
WEL_WINDOW
ensure WEL_WINDOW
result_large_enough: Result >= minimal_width
maximized: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
minimal_height: INTEGER
WEL_WINDOW
ensure WEL_WINDOW
positive_result: Result >= 0
result_small_enough: Result <= maximal_height
minimal_width: INTEGER
WEL_WINDOW
ensure WEL_WINDOW
positive_result: Result >= 0
result_small_enough: Result <= maximal_width
minimized: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
modified: BOOLEAN
require
exists: exists
placement: WEL_WINDOW_PLACEMENT
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
result_not_void: Result /= void
read_only: BOOLEAN
require
exists: exists
selection_end: INTEGER
require
exists: exists
has_selection: has_selection
ensure
result_large_enough: Result >= 0
result_small_enough: Result <= text_length + 2
selection_start: INTEGER
require
exists: exists
has_selection: has_selection
ensure
result_large_enough: Result >= 0
result_small_enough: Result <= text_length
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
shown: BOOLEAN
WEL_WINDOW
require WEL_WINDOW
exists: exists
style: INTEGER
WEL_WINDOW
require WEL_WINDOW
exists: exists
text: STRING
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
result_not_void: Result /= void
text_length: INTEGER
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
positive_result: Result >= 0
valid_color_constant (c: INTEGER): BOOLEAN
c
WEL_COLOR_CONSTANTS
width: INTEGER
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
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
parent = void implies Result = absolute_x
y: INTEGER
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
parent = void implies Result = absolute_y
feature
valid_hwnd_constant (c: POINTER): BOOLEAN
c
WEL_HWND_CONSTANTS
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
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
get_text_limit: INTEGER
require
exisits: exists
ensure
positive_result: Result >= 0
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
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_caret_position (position: INTEGER)
position
require
exists: exists
position_large_enough: position >= 0
position_small_enough: position <= text_length
ensure
has_no_selection: not has_selection
caret_position_set: caret_position = position
set_ex_style (an_ex_style: INTEGER)
an_ex_styleex_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
heavy_capture_activated: heavy_capture_activated
set_modify (modify: BOOLEAN)
modifiedmodify
require
exists: exists
ensure
modified_set: modified = modify
set_read_only
require
exists: exists
set_read_write
require
exists: exists
set_selection (start_position, end_position: INTEGER)
start_position
end_position
require
exists: exists
selection_in_lower_bound: start_position >= 0 and end_position >= 0
selection_in_upper_bound: start_position <= text_length and end_position <= text_length
ensure
has_selection: (start_position /= end_position) implies has_selection
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_style (a_style: INTEGER)
stylea_style
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_text_limit (limit: INTEGER)
limit
require
exists: exists
positive_limit: limit >= 0
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
show
WEL_WINDOW
require WEL_WINDOW
exists: exists
update_cached_style (new_ex_style, old_ex_style: INTEGER)
WEL_WINDOW
feature
has_system_window_locked: BOOLEAN
WEL_WINDOW
lock_window_update
lock_window_update
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
has_system_window_locked
set_font (a_font: WEL_FONT)
fonta_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)
heighta_height
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_item (an_item: POINTER)
iteman_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)
placementa_placement
WEL_WINDOW
require WEL_WINDOW
exists: exists
a_placement_not_void: a_placement /= void
set_text (a_text: STRING)
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
text_set_when_not_void: a_text /= void implies equal (text, a_text)
text_set_when_void: a_text = void implies text.count = 0
set_timer (timer_id, time_out: INTEGER)
timer_id
time_out
on_timerkill_timer
WEL_WINDOW
require WEL_WINDOW
exists: exists
positive_timer_id: timer_id > 0
positive_time_out: time_out > 0
set_width (a_width: INTEGER)
widtha_width
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_x (a_x: INTEGER)
xa_x
WEL_WINDOW
require WEL_WINDOW
exists: exists
set_y (a_y: INTEGER)
ya_y
WEL_WINDOW
require WEL_WINDOW
exists: exists
unlock_window_update
WEL_WINDOW
require WEL_WINDOW
exists: exists
feature
destroy
WEL_WINDOW
require WEL_WINDOW
exists: exists
ensure WEL_WINDOW
not_exists: not exists
dispose
Current
Current
WEL_ANY
feature
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
feature
bring_to_top
WEL_WINDOW
require WEL_WINDOW
exists: exists
clear
WEL_STATIC
require WEL_STATIC
exists: exists
ensure WEL_STATIC
text_empty: text.is_empty
clip_copy
require
exists: exists
has_selection: has_selection
clip_cut
require
exists: exists
has_selection: has_selection
ensure
has_no_selection: not has_selection
clip_paste
require
exists: exists
default_process_notification (notification_code: INTEGER)
notification_code
process_notification
WEL_CONTROL
require WEL_CONTROL
exists: exists
delete_selection
require
exists: exists
has_selection: has_selection
ensure
has_no_selection: not has_selection
disable_horizontal_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
disable_vertical_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
enable_horizontal_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
enable_vertical_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
go_to_next_group_item (a_parent: WEL_COMPOSITE_WINDOW; after: BOOLEAN)
a_parent
after
WEL_CONTROL
require WEL_CONTROL
valid_parent: a_parent /= void and then a_parent.exists
go_to_next_tab_item (a_parent: WEL_COMPOSITE_WINDOW; after: BOOLEAN)
after
WEL_CONTROL
require WEL_CONTROL
valid_parent: a_parent /= void and then a_parent.exists
hide_horizontal_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
hide_scroll_bars
WEL_WINDOW
require WEL_WINDOW
exists: exists
hide_vertical_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
insert_after (a_window: WEL_WINDOW)
a_window
WEL_WINDOW
require WEL_WINDOW
exists: exists
a_window_not_void: a_window /= void
a_window_not_current: a_window /= Current
a_window_exists: a_window.exists
invalidate
WEL_WINDOW
require WEL_WINDOW
exists: exists
invalidate_rect (rect: WEL_RECT; erase_background: BOOLEAN)
rect
erase_background
WEL_WINDOW
require WEL_WINDOW
exists: exists
rect_not_void: rect /= void
invalidate_region (region: WEL_REGION; erase_background: BOOLEAN)
region
erase_background
WEL_WINDOW
require WEL_WINDOW
exists: exists
region_not_void: region /= void
region_exists: region.exists
invalidate_without_background
WEL_WINDOW
require WEL_WINDOW
exists: exists
kill_timer (timer_id: INTEGER)
timer_id
set_timeron_timer
WEL_WINDOW
require WEL_WINDOW
exists: exists
positive_timer_id: timer_id > 0
move (a_x, a_y: INTEGER)
a_xa_y
WEL_WINDOW
require WEL_WINDOW
exists: exists
move_and_resize (a_x, a_y, a_width, a_height: INTEGER; repaint: BOOLEAN)
a_xa_y
a_widtha_height
WEL_WINDOW
require WEL_WINDOW
exists: exists
put_command (a_command: WEL_COMMAND; message: INTEGER; argument: ANY)
a_commandmessage
WEL_WINDOW
require WEL_WINDOW
a_command_not_void: a_command /= void
positive_message: message >= 0
ensure WEL_WINDOW
command_added: command (message) = a_command and command_argument (message) = argument
remove_command (message: INTEGER)
message
WEL_WINDOW
require WEL_WINDOW
positive_message: message >= 0
command_exists: command_exists (message)
ensure WEL_WINDOW
command_removed: not command_exists (message)
replace_selection (new_text: STRING)
new_text
new_text
caret_position
require
exists: exists
new_text_not_void: new_text /= void
resize (a_width, a_height: INTEGER)
a_widtha_height
WEL_WINDOW
require WEL_WINDOW
exists: exists
scroll (a_x, a_y: INTEGER)
a_xa_y
WEL_WINDOW
require WEL_WINDOW
exists: exists
select_all
require
exists: exists
positive_length: text_length > 0
ensure
has_selection: has_selection
selection_start_set: selection_start = 0
selection_end_set: selection_end <= text_length + 2
set_class_icon (new_icon: WEL_ICON)
WEL_WINDOW
set_class_small_icon (new_icon: WEL_ICON)
WEL_WINDOW
set_z_order (z_order: POINTER)
WEL_HWND_CONSTANTSz_order
WEL_WINDOW
require WEL_WINDOW
exists: exists
valid_hwnd_constant: valid_hwnd_constant (z_order)
show_horizontal_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
show_scroll_bars
WEL_WINDOW
require WEL_WINDOW
exists: exists
show_vertical_scroll_bar
WEL_WINDOW
require WEL_WINDOW
exists: exists
show_with_option (cmd_show: INTEGER)
cmd_show
WEL_SW_CONSTANTScmd_show
WEL_WINDOW
require WEL_WINDOW
exists: exists
parent_shown: parent /= void implies parent.exists and parent.shown
undo
require
exists: exists
can_undo: can_undo
unselect
require
exists: exists
has_selection: has_selection
ensure
has_no_selection: not has_selection
update
WEL_WINDOW
require WEL_WINDOW
exists: exists
validate
WEL_WINDOW
require WEL_WINDOW
exists: exists
validate_rect (rect: WEL_RECT)
rect
WEL_WINDOW
require WEL_WINDOW
exists: exists
rect_not_void: rect /= void
validate_region (region: WEL_REGION)
region
WEL_WINDOW
require WEL_WINDOW
exists: exists
region_not_void: region /= void
region_exists: region.exists
win_help (help_file: STRING; a_command, data: INTEGER)
help_file
a_command
WEL_HELP_CONSTANTSa_command
WEL_WINDOW
require WEL_WINDOW
exists: exists
help_file_not_void: help_file /= void
feature
set_default_processing (value: BOOLEAN)
WEL_RETURN_VALUE
ensure WEL_RETURN_VALUE
value_set: default_processing = value
set_message_return_value (value: INTEGER)
WEL_RETURN_VALUE
ensure WEL_RETURN_VALUE
has_return_value: has_return_value
value_set: message_return_value = value
feature
on_en_change
require
exists: exists
on_en_errspace
require
exists: exists
on_en_hscroll
require
exists: exists
on_en_killfocus
require
exists: exists
on_en_maxtext
require
exists: exists
on_en_setfocus
require
exists: exists
on_en_update
require
exists: exists
on_en_vscroll
require
exists: exists
feature
register_current_window
Current
WEL_WINDOW
invariant
consistent_selection: exists and then has_selection implies selection_start >= 0 and then selection_start <= text_length and then selection_end >= 0 and then selection_end <= text_length + 2 and then selection_start < selection_end
valid_caret_position: exists implies caret_position >= 0 and then caret_position <= text_length + 2
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_EDIT