-- Automatic generation produced by ISE Eiffel --
class interface
MAIN_WINDOW
create
make
feature -- Access
artist: ARTIST
artist_button: WEL_PUSH_BUTTON
-- Was declared in MAIN_WINDOW as synonym of maze_button and fun_button.
children: LINKED_LIST [WEL_WINDOW]
-- Construct a linear representation of the children.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
ensure -- from WEL_COMPOSITE_WINDOW
result_not_void: Result /= void
commands: WEL_COMMAND_MANAGER
-- Command manager associated to the current window.
-- (from WEL_WINDOW)
default_processing: BOOLEAN
-- (from WEL_RETURN_VALUE)
fun_button: WEL_PUSH_BUTTON
-- Was declared in MAIN_WINDOW as synonym of maze_button and artist_button.
fun_dialog: FUN_DIALOG
has_return_value: BOOLEAN
-- Should the window procedure return a value?
-- (from WEL_RETURN_VALUE)
item: POINTER
-- Generic Windows handle or structure pointer.
-- Can be a HWND, HICON, RECT *, WNDCLASS *, etc...
-- (from WEL_ANY)
maze: MAZE
maze_button: WEL_PUSH_BUTTON
-- Was declared in MAIN_WINDOW as synonym of artist_button and fun_button.
menu: WEL_MENU
-- Associated menu
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
has_menu: has_menu
ensure -- from WEL_COMPOSITE_WINDOW
result_not_void: Result /= void
message_return_value: INTEGER
-- Return value of the window procedure.
-- (from WEL_RETURN_VALUE)
require -- from WEL_RETURN_VALUE
has_return_value: has_return_value
parent: WEL_WINDOW
-- Parent window
-- (from WEL_WINDOW)
scroller: WEL_SCROLLER
-- Scroller object for processing scroll messages.
-- (from WEL_COMPOSITE_WINDOW)
system_menu: WEL_MENU
-- Associated system menu
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
has_system_menu: has_system_menu
ensure -- from WEL_COMPOSITE_WINDOW
result_not_void: Result /= void
feature -- Status report
absolute_x: INTEGER
-- Absolute x position
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
Result = window_rect.x
absolute_y: INTEGER
-- Absolute y position
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
Result = window_rect.y
background_brush: WEL_BRUSH
-- Current window background color used to refresh the window when
-- requested by the WM_ERASEBKGND windows message.
-- By default there is no background
-- (from WEL_WINDOW)
ensure -- from WEL_WINDOW
new_object: Result /= void implies Result /= background_brush
captured_window: WEL_WINDOW
-- Current window which has been captured.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
window_captured: window_captured
client_rect: WEL_RECT
-- Client rectangle
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
result_not_void: Result /= void
closeable: BOOLEAN
-- Can the user close the window?
-- Yes by default.
-- (from WEL_COMPOSITE_WINDOW)
command (message: INTEGER): WEL_COMMAND
-- Command associated to message
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
positive_message: message >= 0
command_exists: command_exists (message)
ensure -- from WEL_WINDOW
result_not_void: Result /= void
command_argument (message: INTEGER): ANY
-- Command argument associated to message
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
positive_message: message >= 0
command_exists: command_exists (message)
command_exists (message: INTEGER): BOOLEAN
-- Does a command associated to message exist?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
positive_message: message >= 0
commands_enabled: BOOLEAN
-- Is the commands execution enabled?
-- (from WEL_WINDOW)
enabled: BOOLEAN
-- Is the window enabled for mouse and keyboard input?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ex_style: INTEGER
-- Window ex_style
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
exists: BOOLEAN
-- Does the item exist?
-- (from WEL_ANY)
ensure -- from WEL_ANY
Result = (item /= default_pointer)
focused_window: WEL_WINDOW
-- Current window which has the focus.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_capture: BOOLEAN
-- Does this window have the capture?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_focus: BOOLEAN
-- Does this window have the focus?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_heavy_capture: BOOLEAN
-- Does this window have the heavy capture?
-- (from WEL_WINDOW)
has_horizontal_scroll_bar: BOOLEAN
-- Does this window have a horizontal scroll bar?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_menu: BOOLEAN
-- Does the window have a menu?
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
has_system_menu: BOOLEAN
-- Does the window have a system menu?
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
has_vertical_scroll_bar: BOOLEAN
-- Does this window have a vertical scroll bar?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
heavy_capture_activated: BOOLEAN
-- Is the heavy capture currently running?
-- (i.e. is there a window in the current program
-- with has_heavy_capture to True?)
-- (from WEL_WINDOW)
height: INTEGER
-- Window height
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
horizontal_position: INTEGER
-- Current position of the horizontal scroll box
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
ensure -- from WEL_COMPOSITE_WINDOW
result_small_enough: Result <= maximal_horizontal_position
result_large_enough: Result >= minimal_horizontal_position
is_inside: BOOLEAN
-- Is the current window inside another window?
-- (from WEL_WINDOW)
maximal_height: INTEGER
-- Maximal height allowed for the window
-- (from WEL_WINDOW)
ensure -- from WEL_WINDOW
result_large_enough: Result >= minimal_height
maximal_horizontal_position: INTEGER
-- Maxium position of the horizontal scroll box
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
ensure -- from WEL_COMPOSITE_WINDOW
result_large_enough: Result >= minimal_horizontal_position
maximal_vertical_position: INTEGER
-- Maxium position of the vertical scroll box
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
ensure -- from WEL_COMPOSITE_WINDOW
result_large_enough: Result >= minimal_vertical_position
maximal_width: INTEGER
-- Maximal width allowed for the window
-- (from WEL_WINDOW)
ensure -- from WEL_WINDOW
result_large_enough: Result >= minimal_width
maximized: BOOLEAN
-- Is the window maximized?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
minimal_height: INTEGER
-- Minimal height allowed for the window
-- (from WEL_COMPOSITE_WINDOW)
ensure -- from WEL_WINDOW
positive_result: Result >= 0
result_small_enough: Result <= maximal_height
minimal_horizontal_position: INTEGER
-- Minimum position of the horizontal scroll box
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
ensure -- from WEL_COMPOSITE_WINDOW
result_small_enough: Result <= maximal_horizontal_position
minimal_vertical_position: INTEGER
-- Minimum position of the vertical scroll box
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
ensure -- from WEL_COMPOSITE_WINDOW
result_small_enough: Result <= maximal_vertical_position
minimal_width: INTEGER
-- Minimal width allowed for the window
-- (from WEL_COMPOSITE_WINDOW)
ensure -- from WEL_WINDOW
positive_result: Result >= 0
result_small_enough: Result <= maximal_width
minimized: BOOLEAN
-- Is the window minimized?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
placement: WEL_WINDOW_PLACEMENT
-- Window placement information
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
result_not_void: Result /= void
shared: BOOLEAN
-- Is item shared by another object?
-- If False (by default), item will
-- be destroyed by destroy_item.
-- If True, item will not be destroyed.
-- (from WEL_ANY)
shown: BOOLEAN
-- Is the window shown?
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
style: INTEGER
-- Window style
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
text: STRING
-- Window text
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
result_not_void: Result /= void
text_length: INTEGER
-- Text length
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
positive_result: Result >= 0
vertical_position: INTEGER
-- Current position of the vertical scroll box
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
ensure -- from WEL_COMPOSITE_WINDOW
result_small_enough: Result <= maximal_vertical_position
result_large_enough: Result >= minimal_vertical_position
width: INTEGER
-- Window width
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
window_captured: BOOLEAN
-- Has a window been captured?
-- (from WEL_WINDOW)
window_rect: WEL_RECT
-- Window rectangle (absolute position)
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
result_not_void: Result /= void
x: INTEGER
-- Window x position
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
parent = void implies Result = absolute_x
y: INTEGER
-- Window y position
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
parent = void implies Result = absolute_y
feature -- Status report
valid_hwnd_constant (c: POINTER): BOOLEAN
-- Is c a valid hwnd constant?
-- (from WEL_HWND_CONSTANTS)
feature -- Status setting
disable
-- Disable mouse and keyboard input
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
disabled: not enabled
disable_commands
-- Disable commands execution.
-- (from WEL_WINDOW)
ensure -- from WEL_WINDOW
commands_disabled: not commands_enabled
disable_default_processing
-- Disable default window processing.
-- The standard window procedure will not be called for
-- each messages received by the window and then the
-- normal behavior will not occur.
-- (from WEL_WINDOW)
ensure -- from WEL_WINDOW
default_processing_disabled: not default_processing
enable
-- Enable mouse and keyboard input.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
enabled: enabled
enable_commands
-- Enable commands execution.
-- (from WEL_WINDOW)
ensure -- from WEL_WINDOW
commands_enabled: commands_enabled
enable_default_processing
-- Enable default window processing.
-- The standard window procedure will be called for
-- each messages received by the window and then the
-- normal behavior will occur.
-- (from WEL_WINDOW)
ensure -- from WEL_WINDOW
default_processing_enabled: default_processing
hide
-- Hide the window
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
hidden: not shown
horizontal_update (inc, position: INTEGER)
-- Update the window and the horizontal scroll box with
-- inc and position.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
position_small_enough: position <= maximal_horizontal_position
position_large_enough: position >= minimal_horizontal_position
ensure -- from WEL_COMPOSITE_WINDOW
horizontal_position_set: horizontal_position = position
maximize
-- Maximize the window
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
maximized: maximized
minimize
-- Minimize the window and display its icon
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
minimized: minimized
release_capture
-- Release the mouse capture after a call
-- to set_capture.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_capture: has_capture
ensure -- from WEL_WINDOW
not_has_capture: not has_capture
release_heavy_capture
-- Release the mouse capture after a call
-- to set_heavy_capture.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_heavy_capture: has_heavy_capture
heavy_capture_activated: heavy_capture_activated
ensure -- from WEL_WINDOW
heavy_capture_set: not has_heavy_capture
heavy_capture_deactivated: not heavy_capture_activated
restore
-- Restore the window to its
-- original size and position after
-- minimize or maximize
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_capture
-- Set the mouse capture to the Current window.
-- Once the window has captured the mouse, all
-- mouse input is directed to this window, regardless
-- of whether the cursor is over that window. Only
-- one window can have the mouse capture at a time.
--
-- Works only for windows in the same thread as your
-- application.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_not_capture: not has_capture
has_not_heavy_capture: not has_heavy_capture
ensure -- from WEL_WINDOW
has_capture: has_capture
set_ex_style (an_ex_style: INTEGER)
-- Set an_ex_style with ex_style.
--
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_focus
-- Set the focus to Current
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_heavy_capture
-- Set the mouse capture to the Current window.
-- Once the window has captured the mouse, all
-- mouse input is directed to this window, regardless
-- of whether the cursor is over that window. Only
-- one window can have the mouse capture at a time.
--
-- Works for ALL windows.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
has_not_heavy_capture: not has_heavy_capture
heavy_capture_deactivated: not heavy_capture_activated
ensure -- from WEL_WINDOW
heavy_capture_set: has_heavy_capture
heavy_capture_activated: heavy_capture_activated
set_horizontal_position (position: INTEGER)
-- Set horizontal_position with position.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
position_small_enough: position <= maximal_horizontal_position
position_large_enough: position >= minimal_horizontal_position
ensure -- from WEL_COMPOSITE_WINDOW
horizontal_position_set: horizontal_position = position
set_horizontal_range (minimum, maximum: INTEGER)
-- Set minimal_horizontal_position and
-- maximal_horizontal_position with minimum and
-- maximum.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
consistent_range: minimum <= maximum
ensure -- from WEL_COMPOSITE_WINDOW
minimal_horizontal_position_set: minimal_horizontal_position = minimum
maximal_horizontal_position_set: maximal_horizontal_position = maximum
set_icon (a_small_icon: WEL_ICON; a_big_icon: WEL_ICON)
-- Set the small (16x16) and the normal (32x32) icon for this window.
--
-- Note: Set a_small_icon to Void to remove the small icon and
-- a_big_icon to Void to remove the big icon.
-- (from WEL_COMPOSITE_WINDOW)
set_menu (a_menu: WEL_MENU)
-- Set menu with a_menu.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
a_menu_not_void: a_menu /= void
a_menu_exists: a_menu.exists
ensure -- from WEL_COMPOSITE_WINDOW
has_menu: has_menu
menu_set: menu.item = a_menu.item
set_shared
-- Set shared to True.
-- (from WEL_ANY)
ensure -- from WEL_ANY
shared: shared
set_style (a_style: INTEGER)
-- Set style with a_style.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_unshared
-- Set shared to False.
-- (from WEL_ANY)
ensure -- from WEL_ANY
unshared: not shared
set_vertical_position (position: INTEGER)
-- Set vertical_position with position.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
position_small_enough: position <= maximal_vertical_position
position_large_enough: position >= minimal_vertical_position
ensure -- from WEL_COMPOSITE_WINDOW
vertical_position_set: vertical_position = position
set_vertical_range (minimum, maximum: INTEGER)
-- Set minimal_vertical_position and
-- maximal_vertical_position with minimum and
-- maximum.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
scroller_exists: scroller /= void
consistent_range: minimum <= maximum
ensure -- from WEL_COMPOSITE_WINDOW
minimal_vertical_position_set: minimal_vertical_position = minimum
maximal_vertical_position_set: maximal_vertical_position = maximum
show
-- Show the window
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
unset_menu
-- Unset the current menu associated to the window.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
ensure -- from WEL_COMPOSITE_WINDOW
menu_unset: not has_menu
update_cached_style (new_ex_style, old_ex_style: INTEGER)
-- Update Window cache buffer for Window style.
--
-- (from WEL_WINDOW)
vertical_update (inc, position: INTEGER)
-- Update the window and the vertical scroll box with
-- inc and position.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
position_small_enough: position <= maximal_vertical_position
position_large_enough: position >= minimal_vertical_position
ensure -- from WEL_COMPOSITE_WINDOW
vertical_position_set: vertical_position = position
feature -- Element change
has_system_window_locked: BOOLEAN
-- Is there any window locked ?
-- (from WEL_WINDOW)
lock_window_update
-- Disables drawing in the current window. A locked window cannot be moved.
-- Only one window can be locked at a time. To unlock a window locked with
-- lock_window_update , call 'unlock_window_update'.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
has_system_window_locked
set_height (a_height: INTEGER)
-- Set height with a_height
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_item (an_item: POINTER)
-- Set item with an_item
-- (from WEL_ANY)
ensure -- from WEL_ANY
item_set: item = an_item
set_parent (a_parent: WEL_WINDOW)
-- Change the parent of the current window.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_placement (a_placement: WEL_WINDOW_PLACEMENT)
-- Set placement with a_placement
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
a_placement_not_void: a_placement /= void
set_text (a_text: STRING)
-- Set the window text
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from 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)
-- Set a timer identified by timer_id with a
-- time_out value (in milliseconds).
-- See also on_timer, kill_timer.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
positive_timer_id: timer_id > 0
positive_time_out: time_out > 0
set_width (a_width: INTEGER)
-- Set width with a_width
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_x (a_x: INTEGER)
-- Set x with a_x
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_y (a_y: INTEGER)
-- Set y with a_y
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
unlock_window_update
-- Unlock a locked window.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
feature -- Removal
dispose
-- Destroy the inner structure of Current.
--
-- This function should be called by the GC when the
-- object is collected or by the user if Current is
-- no more usefull.
-- (from WEL_ANY)
feature -- Conversion
to_integer: INTEGER
-- Converts item to an integer.
-- (from WEL_ANY)
ensure -- from WEL_ANY
Result = cwel_pointer_to_integer (item)
feature -- Basic operations
bring_to_top
-- Bring this window to the top of the Z order.
--
-- Note:
-- * If the window is a top-level window, it is activated.
-- * If the window is a child window, the top-level parent window
-- associated with the child window is activated.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
destroy
-- Destroy the window and quit the application
-- if Current is the application's main window.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_WINDOW
exists: exists
ensure -- from WEL_WINDOW
not_exists: not exists
disable_horizontal_scroll_bar
-- Disable the horizontal scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
disable_vertical_scroll_bar
-- Disable the vertical scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
draw_menu
-- Draw the menu bar associated with the window.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
has_menu: has_menu
enable_horizontal_scroll_bar
-- Enable the horizontal scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
enable_vertical_scroll_bar
-- Enable the vertical scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
hide_horizontal_scroll_bar
-- Hide the horizontal scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
hide_scroll_bars
-- Hide the horizontal and vertical scroll bars.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
hide_vertical_scroll_bar
-- Hide the vertical scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
insert_after (a_window: WEL_WINDOW)
-- Insert the current window after a_window.
-- (from WEL_WINDOW)
require -- from 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
-- Invalide the entire client area of the window. The
-- background will be erased before.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
invalidate_rect (rect: WEL_RECT; erase_background: BOOLEAN)
-- Invalidate the area rect and erase
-- the background if erase_background is True.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
rect_not_void: rect /= void
invalidate_region (region: WEL_REGION; erase_background: BOOLEAN)
-- Invalidate the area region and erase
-- the background if erase_background is True.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
region_not_void: region /= void
region_exists: region.exists
invalidate_without_background
-- Invalidate the entire client area of the window. The
-- background will not be erased.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
kill_timer (timer_id: INTEGER)
-- Kill the timer identified by timer_id.
-- See also set_timer, on_timer.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
positive_timer_id: timer_id > 0
move (a_x, a_y: INTEGER)
-- Move the window to a_x, a_y position.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_WINDOW
exists: exists
move_absolute (a_x, a_y: INTEGER)
-- Move the window to a_x, a_y absolute position.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_COMPOSITE_WINDOW
exists: exists
move_and_resize (a_x, a_y, a_width, a_height: INTEGER; repaint: BOOLEAN)
-- Move the window to a_x, a_y position and
-- resize it with a_width, a_height.
-- (from WEL_COMPOSITE_WINDOW)
require -- from WEL_WINDOW
exists: exists
put_command (a_command: WEL_COMMAND; message: INTEGER; argument: ANY)
-- Put a_command associated to message.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
a_command_not_void: a_command /= void
positive_message: message >= 0
ensure -- from WEL_WINDOW
command_added: command (message) = a_command and command_argument (message) = argument
remove_command (message: INTEGER)
-- Remove the command associated to message.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
positive_message: message >= 0
command_exists: command_exists (message)
ensure -- from WEL_WINDOW
command_removed: not command_exists (message)
resize (a_width, a_height: INTEGER)
-- Resize the window with a_width, a_height.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
scroll (a_x, a_y: INTEGER)
-- Scroll the contents of the window's client area.
-- a_x and a_y specify the amount of horizontal
-- and vertical scrolling.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
set_class_icon (new_icon: WEL_ICON)
-- Replace the current icon for the class which this window
-- belongs to.
--
-- The SetClassLong function replaces the specified 32-bit (long)
-- value at the specified offset into the extra class memory
-- or the WNDCLASSEX structure for the class to which the
-- specified window belongs.
-- (from WEL_WINDOW)
set_class_small_icon (new_icon: WEL_ICON)
-- Replace the current icon for the class which this window
-- belongs to.
--
-- The SetClassLong function replaces the specified 32-bit (long)
-- value at the specified offset into the extra class memory
-- or the WNDCLASSEX structure for the class to which the
-- specified window belongs.
-- (from WEL_WINDOW)
set_z_order (z_order: POINTER)
-- Set the z-order of the window.
-- See class WEL_HWND_CONSTANTS for z_order values.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
valid_hwnd_constant: valid_hwnd_constant (z_order)
show_horizontal_scroll_bar
-- Show the horizontal scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
show_scroll_bars
-- Show the horizontal and vertical scroll bars.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
show_vertical_scroll_bar
-- Show the vertical scroll bar.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
show_with_option (cmd_show: INTEGER)
-- Set the window's visibility with cmd_show.
-- See class WEL_SW_CONSTANTS for cmd_show value.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
parent_shown: parent /= void implies parent.exists and parent.shown
update
-- Update the client area by sending a Wm_paint message.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
validate_rect (rect: WEL_RECT)
-- Validate the area rect.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
rect_not_void: rect /= void
validate_region (region: WEL_REGION)
-- Validate the area region.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
region_not_void: region /= void
region_exists: region.exists
win_help (help_file: STRING; a_command, data: INTEGER)
-- Start the Windows Help program with help_file.
-- a_command specifies the type of help requested. See
-- class WEL_HELP_CONSTANTS for a_command values.
-- 'data' is depandant on 'a_command'. Check MSDN for more details.
-- (from WEL_WINDOW)
require -- from WEL_WINDOW
exists: exists
help_file_not_void: help_file /= void
feature -- Default creation values
default_height: INTEGER
-- Default position and dimension when the window is
-- created.
-- Was declared in WEL_FRAME_WINDOW as synonym of default_x, default_y and default_width.
-- (from WEL_FRAME_WINDOW)
default_id: INTEGER
-- Default window id.
-- (Zero by default).
-- (from WEL_FRAME_WINDOW)
default_style: INTEGER
-- Overlapped window style.
-- By default, a frame window is not visible
-- at the creation time. show needs to be called.
-- This solution avoids a bad visual effect when
-- the children are created one by one inside
-- the window.
-- (from WEL_FRAME_WINDOW)
default_width: INTEGER
-- Default position and dimension when the window is
-- created.
-- Was declared in WEL_FRAME_WINDOW as synonym of default_x, default_y and default_height.
-- (from WEL_FRAME_WINDOW)
default_x: INTEGER
-- Default position and dimension when the window is
-- created.
-- Was declared in WEL_FRAME_WINDOW as synonym of default_y, default_width and default_height.
-- (from WEL_FRAME_WINDOW)
default_y: INTEGER
-- Default position and dimension when the window is
-- created.
-- Was declared in WEL_FRAME_WINDOW as synonym of default_x, default_width and default_height.
-- (from WEL_FRAME_WINDOW)
feature -- Element Change
set_default_processing (value: BOOLEAN)
-- Enable or disable default processing of window messages.
-- (from WEL_RETURN_VALUE)
ensure -- from WEL_RETURN_VALUE
value_set: default_processing = value
set_message_return_value (value: INTEGER)
-- Set the window-procedure-return-value.
-- (from WEL_RETURN_VALUE)
ensure -- from WEL_RETURN_VALUE
has_return_value: has_return_value
value_set: message_return_value = value
feature -- Registration
register_current_window
-- Register Current in window manager.
-- (from WEL_WINDOW)
feature -- Standard window class values
class_background: WEL_BRUSH
-- Standard window background color used to create the
-- window class.
-- Can be redefined to return a user-defined brush.
-- (from WEL_FRAME_WINDOW)
require -- from WEL_FRAME_WINDOW
background_brush_not_set: background_brush = void
ensure -- from WEL_FRAME_WINDOW
result_not_void: Result /= void
class_cursor: WEL_CURSOR
-- Standard arrow cursor used to create the window
-- class.
-- Can be redefined to return a user-defined cursor.
-- (from WEL_FRAME_WINDOW)
ensure -- from WEL_FRAME_WINDOW
result_not_void: Result /= void
result_exists: Result.exists
class_menu_name: STRING
-- Window's menu used to create the window class.
-- Can be redefined to return a user-defined menu.
-- (None by default).
-- (from WEL_FRAME_WINDOW)
ensure -- from WEL_FRAME_WINDOW
result_not_void: Result /= void
class_name: STRING
-- Window class name used to create the window class.
-- Can be redefined to return a user-defined class name.
-- (from WEL_FRAME_WINDOW)
ensure -- from WEL_WINDOW
result_not_void: Result /= void
class_style: INTEGER
-- Standard style used to create the window class.
-- Can be redefined to return a user-defined style.
-- (from WEL_FRAME_WINDOW)
class_window_procedure: POINTER
-- Standard window procedure
-- (from WEL_FRAME_WINDOW)
ensure -- from WEL_FRAME_WINDOW
result_not_null: Result /= default_pointer
invariant
-- from ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- class MAIN_WINDOW
-- Generated by ISE Eiffel --
-- For more details: www.eiffel.com --