indexing
	description: "MDI frame window containing a MDI client window."
	status: "See notice at end of class."
	date: "$Date$"
	revision: "$Revision$"
class interface
	WEL_MDI_FRAME_WINDOW
create 
	make_top (a_name: STRING; a_menu: WEL_MENU; first_child: INTEGER)
			a_name
			a_menu
			first_child
			
			
			
			on_command_control_id
			
			
			
		require
			a_name_not_void: a_name /= void
			a_menu_not_void: a_menu /= void
			a_menu_exists: a_menu.exists
		ensure
			parent_set: parent = void
			exists: exists
			name_set: text.is_equal (a_name)
			client_window_not_void: client_window /= void
			client_window_exists: client_window.exists
feature 
	children: LIST [WEL_WINDOW]
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
		ensure  WEL_COMPOSITE_WINDOW
			result_not_void: Result /= void
	client_window: WEL_MDI_CLIENT_WINDOW
			
	commands: WEL_COMMAND_MANAGER
			
			 WEL_WINDOW
	default_processing: BOOLEAN
			 WEL_RETURN_VALUE
	has_return_value: BOOLEAN
			
			 WEL_RETURN_VALUE
	item: POINTER
			
			
			 WEL_ANY
	menu: WEL_MENU
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			has_menu: has_menu
		ensure  WEL_COMPOSITE_WINDOW
			result_not_void: Result /= void
	message_return_value: INTEGER
			
			 WEL_RETURN_VALUE
		require  WEL_RETURN_VALUE
			has_return_value: has_return_value
	parent: WEL_WINDOW
			
			 WEL_WINDOW
	scroller: WEL_SCROLLER
			
			 WEL_COMPOSITE_WINDOW
	system_menu: WEL_MENU
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			has_system_menu: has_system_menu
		ensure  WEL_COMPOSITE_WINDOW
			result_not_void: Result /= void
	
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
	active_window: WEL_MDI_CHILD_WINDOW
			
		require
			exists: exists
			client_window_not_void: client_window /= void
			client_window_exists: client_window.exists
			has_active_window: has_active_window
	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
	closeable: BOOLEAN
			
			
			 WEL_COMPOSITE_WINDOW
	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
	has_active_window: BOOLEAN
			
		require
			exists: exists
			client_window_not_void: client_window /= void
			client_window_exists: client_window.exists
	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_menu: BOOLEAN
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
	has_system_menu: BOOLEAN
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			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
	horizontal_position: INTEGER
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
		ensure  WEL_COMPOSITE_WINDOW
			result_small_enough: Result <= maximal_horizontal_position
			result_large_enough: Result >= minimal_horizontal_position
	is_inside: BOOLEAN
			
			 WEL_WINDOW
	maximal_height: INTEGER
			
			 WEL_WINDOW
		ensure  WEL_WINDOW
			result_large_enough: Result >= minimal_height
	maximal_horizontal_position: INTEGER
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
		ensure  WEL_COMPOSITE_WINDOW
			result_large_enough: Result >= minimal_horizontal_position
	maximal_vertical_position: INTEGER
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
		ensure  WEL_COMPOSITE_WINDOW
			result_large_enough: Result >= minimal_vertical_position
	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_COMPOSITE_WINDOW
		ensure  WEL_WINDOW
			positive_result: Result >= 0
			result_small_enough: Result <= maximal_height
	minimal_horizontal_position: INTEGER
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
		ensure  WEL_COMPOSITE_WINDOW
			result_small_enough: Result <= maximal_horizontal_position
	minimal_vertical_position: INTEGER
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
		ensure  WEL_COMPOSITE_WINDOW
			result_small_enough: Result <= maximal_vertical_position
	minimal_width: INTEGER
			
			 WEL_COMPOSITE_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
	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
	vertical_position: INTEGER
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
		ensure  WEL_COMPOSITE_WINDOW
			result_small_enough: Result <= maximal_vertical_position
			result_large_enough: Result >= minimal_vertical_position
	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
	hide
			
			 WEL_WINDOW
		require  WEL_WINDOW
			exists: exists
		ensure  WEL_WINDOW
			hidden: not shown
	horizontal_update (inc, position: INTEGER)
			
			incposition
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			position_small_enough: position <= maximal_horizontal_position
			position_large_enough: position >= minimal_horizontal_position
		ensure  WEL_COMPOSITE_WINDOW
			horizontal_position_set: horizontal_position = position
	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_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_horizontal_position (position: INTEGER)
			horizontal_positionposition
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
			position_small_enough: position <= maximal_horizontal_position
			position_large_enough: position >= minimal_horizontal_position
		ensure  WEL_COMPOSITE_WINDOW
			horizontal_position_set: horizontal_position = position
	set_horizontal_range (minimum, maximum: INTEGER)
			minimal_horizontal_position
			maximal_horizontal_positionminimum
			maximum
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
			consistent_range: minimum <= maximum
		ensure  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)
			
			
			a_small_icon
			a_big_icon
			 WEL_COMPOSITE_WINDOW
	set_menu (a_menu: WEL_MENU)
			menua_menu
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			a_menu_not_void: a_menu /= void
			a_menu_exists: a_menu.exists
		ensure  WEL_COMPOSITE_WINDOW
			has_menu: has_menu
			menu_set: menu.item = a_menu.item
	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_unshared
			shared
			 WEL_ANY
		ensure  WEL_ANY
			unshared: not shared
	set_vertical_position (position: INTEGER)
			vertical_positionposition
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
			position_small_enough: position <= maximal_vertical_position
			position_large_enough: position >= minimal_vertical_position
		ensure  WEL_COMPOSITE_WINDOW
			vertical_position_set: vertical_position = position
	set_vertical_range (minimum, maximum: INTEGER)
			minimal_vertical_position
			maximal_vertical_positionminimum
			maximum
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			scroller_exists: scroller /= void
			consistent_range: minimum <= maximum
		ensure  WEL_COMPOSITE_WINDOW
			minimal_vertical_position_set: minimal_vertical_position = minimum
			maximal_vertical_position_set: maximal_vertical_position = maximum
	show
			
			 WEL_WINDOW
		require  WEL_WINDOW
			exists: exists
	unset_menu
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
		ensure  WEL_COMPOSITE_WINDOW
			menu_unset: not has_menu
	update_cached_style (new_ex_style, old_ex_style: INTEGER)
			
			 WEL_WINDOW
	vertical_update (inc, position: INTEGER)
			
			incposition
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			position_small_enough: position <= maximal_vertical_position
			position_large_enough: position >= minimal_vertical_position
		ensure  WEL_COMPOSITE_WINDOW
			vertical_position_set: vertical_position = position
	
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_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 
	dispose
			Current
			
			
			Current
			
			 WEL_ANY
	
feature 
	to_integer: INTEGER
			item
			 WEL_ANY
		ensure  WEL_ANY
			Result = cwel_pointer_to_integer (item)
	
feature 
	arrange_icons
			
		require
			exists: exists
	bring_to_top
			
			
			
			
			
			
			 WEL_WINDOW
		require  WEL_WINDOW
			exists: exists
	cascade_children
			
		require
			exists: exists
	destroy
			
			Current
			 WEL_COMPOSITE_WINDOW
		require  WEL_WINDOW
			exists: exists
		ensure  WEL_WINDOW
			not_exists: not exists
	disable_horizontal_scroll_bar
			
			 WEL_WINDOW
		require  WEL_WINDOW
			exists: exists
	disable_vertical_scroll_bar
			
			 WEL_WINDOW
		require  WEL_WINDOW
			exists: exists
	draw_menu
			
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
			has_menu: has_menu
	enable_horizontal_scroll_bar
			
			 WEL_WINDOW
		require  WEL_WINDOW
			exists: exists
	enable_vertical_scroll_bar
			
			 WEL_WINDOW
		require  WEL_WINDOW
			exists: 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_COMPOSITE_WINDOW
		require  WEL_WINDOW
			exists: exists
	move_absolute (a_x, a_y: INTEGER)
			a_xa_y
			 WEL_COMPOSITE_WINDOW
		require  WEL_COMPOSITE_WINDOW
			exists: exists
	move_and_resize (a_x, a_y, a_width, a_height: INTEGER; repaint: BOOLEAN)
			a_xa_y
			a_widtha_height
			 WEL_COMPOSITE_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)
	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
	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
	tile_children_horizontal
			
		require
			exists: exists
	tile_children_vertical
			
		require
			exists: exists
	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 
	default_height: INTEGER
			
			
			WEL_FRAME_WINDOWdefault_xdefault_ydefault_width
			 WEL_FRAME_WINDOW
	default_id: INTEGER
			
			
			 WEL_FRAME_WINDOW
	default_style: INTEGER
			
			
			show
			
			
			
			 WEL_FRAME_WINDOW
	default_width: INTEGER
			
			
			WEL_FRAME_WINDOWdefault_xdefault_ydefault_height
			 WEL_FRAME_WINDOW
	default_x: INTEGER
			
			
			WEL_FRAME_WINDOWdefault_ydefault_widthdefault_height
			 WEL_FRAME_WINDOW
	default_y: INTEGER
			
			
			WEL_FRAME_WINDOWdefault_xdefault_widthdefault_height
			 WEL_FRAME_WINDOW
	
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 
	register_current_window
			Current
			 WEL_WINDOW
	
feature 
	class_cursor: WEL_CURSOR
			
			
			
			 WEL_FRAME_WINDOW
		ensure  WEL_FRAME_WINDOW
			result_not_void: Result /= void
			result_exists: Result.exists
	class_icon: WEL_ICON
			
			
			
			 WEL_FRAME_WINDOW
		ensure  WEL_FRAME_WINDOW
			result_not_void: Result /= void
			result_exists: Result.exists
	class_menu_name: STRING
			
			
			
			 WEL_FRAME_WINDOW
		ensure  WEL_FRAME_WINDOW
			result_not_void: Result /= void
	class_style: INTEGER
			
			
			 WEL_FRAME_WINDOW
	class_window_procedure: POINTER
			
			 WEL_FRAME_WINDOW
		ensure  WEL_FRAME_WINDOW
			result_not_null: Result /= default_pointer
	
invariant
		 ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
end -- WEL_MDI_FRAME_WINDOW