MAIN_WINDOW Flat contracts

indexing
description: "The main window for the vision2 widget test."
date: "$Date$"
revision: "$Revision$"

class interface
MAIN_WINDOW

create

frozen default_create
-- Standard creation procedure.
-- (from EV_ANY)
ensure then -- from EV_ANY
is_coupled: implementation /= void
is_initialized: is_initialized
default_create_called_set: default_create_called
is_in_default_state: is_in_default_state

feature -- Initialization

frozen default_create
-- Standard creation procedure.
-- (from EV_ANY)
ensure then -- from EV_ANY
is_coupled: implementation /= void
is_initialized: is_initialized
default_create_called_set: default_create_called
is_in_default_state: is_in_default_state

feature -- Access

a_menu_bar: EV_MENU_BAR

about_dialog: ABOUT_DIALOG

about_menu_item: EV_MENU_ITEM
-- Was declared in MAIN_WINDOW as synonym of exit_menu_item.

accelerators: EV_ACCELERATOR_LIST
-- Key combination shortcuts associated with this window.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed

accept_cursor: EV_CURSOR
-- Result is cursor displayed when the screen pointer is over a
-- target that accepts pebble during pick and drop.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.accept_cursor

actual_drop_target_agent: FUNCTION [ANY, TUPLE [INTEGER, INTEGER], EV_ABSTRACT_PICK_AND_DROPABLE]
-- Overrides default drop target on a certain position.
-- If Void, Current will use the default drop target.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.actual_drop_target_agent

background_color: EV_COLOR
-- Color displayed behind foreground features.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure -- from EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.background_color)

Bit_type: INTEGER is 8
-- (from INTERNAL)

boolean_field (i: INTEGER; object: ANY): BOOLEAN
-- Boolean value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
boolean_field: field_type (i, object) = boolean_type

Boolean_type: INTEGER is 3
-- (from INTERNAL)

button: EV_BUTTON
-- Was declared in MAIN_WINDOW as synonym of button1.

button1: EV_BUTTON
-- Was declared in MAIN_WINDOW as synonym of button.

character_field (i: INTEGER; object: ANY): CHARACTER
-- Character value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
character_field: field_type (i, object) = character_type

Character_type: INTEGER is 2
-- (from INTERNAL)

class_name (object: ANY): STRING
-- Name of the class associated with object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

data: ANY
-- Arbitrary user data may be stored here.
-- (from EV_ANY)

deny_cursor: EV_CURSOR
-- Result is cursor displayed when the screen pointer is over a
-- target that does not accept pebble during pick and drop.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.deny_cursor

double_field (i: INTEGER; object: ANY): DOUBLE
-- Double precision value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
double_field: field_type (i, object) = double_type

Double_type: INTEGER is 6
-- (from INTERNAL)

dynamic_type (object: ANY): INTEGER
-- Dynamic type of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

exit_menu_item: EV_MENU_ITEM
-- Was declared in MAIN_WINDOW as synonym of about_menu_item.

expanded_field_type (i: INTEGER; object: ANY): STRING
-- Class name associated with the i-th
-- expanded field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
is_expanded: field_type (i, object) = expanded_type
ensure -- from INTERNAL
result_exists: Result /= void

Expanded_type: INTEGER is 7
-- (from INTERNAL)

field (i: INTEGER; object: ANY): ANY
-- Object attached to the i-th field of object
-- (directly or through a reference)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
not_special: not is_special (object)

field_name (i: INTEGER; object: ANY): STRING
-- Name of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
not_special: not is_special (object)
ensure -- from INTERNAL
result_exists: Result /= void

field_name_of_type (i: INTEGER; type_id: INTEGER): STRING
-- Name of i-th field of dynamic type type_id.
-- (from INTERNAL)
require -- from INTERNAL
index_large_enough: i >= 1
index_small_enought: i <= field_count_of_type (type_id)

field_offset (i: INTEGER; object: ANY): INTEGER
-- Offset of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
not_special: not is_special (object)

field_type (i: INTEGER; object: ANY): INTEGER
-- Type of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)

field_type_of_type (i: INTEGER; type_id: INTEGER): INTEGER
-- Type of i-th field of dynamic type type_id
-- (from INTERNAL)
require -- from INTERNAL
index_large_enough: i >= 1
index_small_enough: i <= field_count_of_type (type_id)

file_menu: EV_MENU
-- Was declared in MAIN_WINDOW as synonym of help_menu.

foreground_color: EV_COLOR
-- Color of foreground features like text.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure -- from EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.foreground_color)

frame: EV_FRAME

generic_dynamic_type (object: ANY; i: INTEGER): INTEGER
-- Dynamic type of generic parameter of object at
-- position i.
-- (from INTERNAL)

has_recursive (an_item: like item): BOOLEAN
-- Does structure include an_item or
-- does any structure recursivly included by structure,
-- include an_item.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed

help_context: FUNCTION [ANY, TUPLE, EV_HELP_CONTEXT]
-- Agent that evaluates to help context sent to help engine when help is requested
-- (from EV_HELP_CONTEXTABLE)
require -- from EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
ensure -- from EV_HELP_CONTEXTABLE
bridge_ok: Result = implementation.help_context

help_menu: EV_MENU
-- Was declared in MAIN_WINDOW as synonym of file_menu.

horizontal_box: EV_HORIZONTAL_BOX

icon_name: STRING
-- Alternative name, displayed when window is minimised.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_TITLED_WINDOW
bridge_ok: equal (Result, implementation.icon_name)

icon_pixmap: EV_PIXMAP
-- Window icon.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_TITLED_WINDOW
bridge_ok: Result.is_equal (implementation.icon_pixmap)

frozen id_object (an_id: INTEGER): IDENTIFIED
-- Object associated with an_id (void if no such object)
-- (from IDENTIFIED)
ensure -- from IDENTIFIED
consistent: Result = void or else Result.object_id = an_id

Integer_16_type: INTEGER is 10
-- (from INTERNAL)

Integer_32_type: INTEGER is 4
-- (from INTERNAL)

Integer_64_type: INTEGER is 11
-- (from INTERNAL)

Integer_8_type: INTEGER is 9
-- (from INTERNAL)

integer_field (i: INTEGER; object: ANY): INTEGER
-- Integer value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_field: field_type (i, object) = integer_type

Integer_type: INTEGER is 4
-- (from INTERNAL)

is_parent_recursive (a_widget: EV_WIDGET): BOOLEAN
-- Is a_widget parent, or recursivly, parent of parent.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed

item: EV_WIDGET
-- Current item.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
readable: readable
ensure -- from EV_CONTAINER
bridge_ok: Result = implementation.item

lower_bar: EV_VERTICAL_BOX
-- Room at bottom of window. (Example use: statusbar.)
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
bridge_ok: Result = implementation.lower_bar

maximum_height: INTEGER
-- Upper bound on height in pixels.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
bridge_ok: (Result = implementation.internal_maximum_height) or (Result = implementation.minimum_height)

maximum_width: INTEGER
-- Upper bound on width in pixels.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
bridge_ok: (Result = implementation.internal_maximum_width) or (Result = implementation.minimum_width)

menu_bar: EV_MENU_BAR
-- Horizontal bar at top of client area that contains menu's.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
bridge_ok: Result = implementation.menu_bar

frozen object_id: INTEGER
-- Unique for current object in any given session
-- (from IDENTIFIED)
ensure -- from IDENTIFIED
valid_id: id_object (Result) = Current

output: EV_TEXT
-- All event output occurs here.
-- The following widgets are used to build the interface
-- for the user.

parent: EV_CONTAINER
-- Contains Current.
-- (from EV_WIDGET)
require -- from EV_CONTAINABLE
not_destroyed: not is_destroyed
ensure then -- from EV_WIDGET
bridge_ok: Result = implementation.parent

pebble: ANY
-- Data to be transported by pick and drop mechanism.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble

pebble_function: FUNCTION [ANY, TUPLE, ANY]
-- Returns data to be transported by pick and drop mechanism.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_function

pebble_positioning_enabled: BOOLEAN
-- If True then pick and drop start coordinates are
-- pebble_x_position, pebble_y_position.
-- If False then pick and drop start coordinates are
-- the pointer coordinates.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_positioning_enabled

pebble_x_position: INTEGER
-- Initial x position for pick and drop relative to Current.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_x_position

pebble_y_position: INTEGER
-- Initial y position for pick and drop relative to Current.
-- (from EV_PICK_AND_DROPABLE)
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_y_position

pointer_field (i: INTEGER; object: ANY): POINTER
-- Pointer value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
pointer_field: field_type (i, object) = pointer_type

pointer_position: EV_COORDINATE
-- Position of the screen pointer relative to Current.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
is_show_requested: is_show_requested

pointer_style: EV_CURSOR
-- Cursor displayed when pointer is over this widget.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed

Pointer_type: INTEGER is 0
-- (from INTERNAL)

real_field (i: INTEGER; object: ANY): REAL
-- Real value of i-th field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_field: field_type (i, object) = real_type

Real_type: INTEGER is 5
-- (from INTERNAL)

Reference_type: INTEGER is 1
-- (from INTERNAL)

scrollable_area: EV_SCROLLABLE_AREA

target_name: STRING
-- Optional textual name describing Current pick and drop hole.
-- (from EV_ABSTRACT_PICK_AND_DROPABLE)

test_detail_selection: EV_NOTEBOOK
-- This holds different details of the test for each widget.

test_holder: EV_VERTICAL_BOX

text_field: EV_TEXT_FIELD

title: STRING
-- A textual name used by the window manager.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
bridge_ok: equal (Result, implementation.title)

upper_bar: EV_VERTICAL_BOX
-- Room at top of window. (Example use: toolbars.)
-- Positioned below menu bar.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
bridge_ok: Result = implementation.upper_bar

vertical_box: EV_VERTICAL_BOX
-- Was declared in MAIN_WINDOW as synonym of vertical_box1.

vertical_box1: EV_VERTICAL_BOX
-- Was declared in MAIN_WINDOW as synonym of vertical_box.

Wide_character_type: INTEGER is 12
-- (from INTERNAL)

widget_area: EV_FRAME
-- A cell to hold the currently selected and testable widget.

widget_tree: EV_TREE
-- A tree holding all testable widgets.

feature -- Measurement

bit_size (i: INTEGER; object: ANY): INTEGER
-- Size (in bit) of the i-th bit field of object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
is_bit: field_type (i, object) = bit_type
ensure -- from INTERNAL
positive_result: Result > 0

client_height: INTEGER
-- Height of the area available to children in pixels.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
ensure -- from EV_CONTAINER
bridge_ok: Result = implementation.client_height

client_width: INTEGER
-- Width of the area available to children in pixels.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
ensure -- from EV_CONTAINER
bridge_ok: Result = implementation.client_width

field_count (object: ANY): INTEGER
-- Number of logical fields in object
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

field_count_of_type (type_id: INTEGER): INTEGER
-- Number of logical fields in dynamic type type_id.
-- (from INTERNAL)

height: INTEGER
-- Vertical size in pixels.
-- Same as minimum_height when not displayed.
-- (from EV_POSITIONED)
require -- from EV_POSITIONED
not_destroyed: not is_destroyed
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.height

minimum_height: INTEGER
-- Lower bound on height in pixels.
-- (from EV_POSITIONED)
require -- from EV_POSITIONED
not_destroyed: not is_destroyed
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.minimum_height
positive_or_zero: Result >= 0

minimum_width: INTEGER
-- Lower bound on width in pixels.
-- (from EV_POSITIONED)
require -- from EV_POSITIONED
not_destroyed: not is_destroyed
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.minimum_width
positive_or_zero: Result >= 0

physical_size (object: ANY): INTEGER
-- Space occupied by object in bytes
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

screen_x: INTEGER
-- Horizontal offset relative to left of screen in pixels.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.screen_x

screen_y: INTEGER
-- Vertical offset relative to top of screen in pixels.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.screen_y

width: INTEGER
-- Horizontal size in pixels.
-- Same as minimum_width when not displayed.
-- (from EV_POSITIONED)
require -- from EV_POSITIONED
not_destroyed: not is_destroyed
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.width

x_position: INTEGER
-- Horizontal offset relative to parent x_position in pixels.
-- (from EV_POSITIONED)
require -- from EV_POSITIONED
not_destroyed: not is_destroyed
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.x_position

y_position: INTEGER
-- Vertical offset relative to parent y_position in pixels.
-- (from EV_POSITIONED)
require -- from EV_POSITIONED
not_destroyed: not is_destroyed
ensure -- from EV_POSITIONED
bridge_ok: Result = implementation.y_position

feature -- Status report

count: INTEGER
-- Number of items in Current.
-- (from EV_CELL)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
ensure then -- from EV_CELL
valid_result: Result = 0 or Result = 1

extendible: BOOLEAN
-- Is there no element?
-- Was declared in EV_CELL as synonym of is_empty.
-- (from EV_CELL)

full: BOOLEAN
-- Is structure filled to capacity?
-- (from EV_CELL)

has (v: EV_WIDGET): BOOLEAN
-- Does structure include v?
-- (from EV_WINDOW)
ensure -- from CONTAINER
not_found_in_empty: Result implies not is_empty

has_capture: BOOLEAN
-- Does widget have capture?
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.has_capture

has_focus: BOOLEAN
-- Does widget have the keyboard focus?
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.has_focus

is_displayed: BOOLEAN
-- Is Current visible on the screen?
-- True when show requested and parent displayed.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.is_displayed

is_empty: BOOLEAN
-- Is there no element?
-- Was declared in EV_CELL as synonym of extendible.
-- (from EV_CELL)

is_inserted (v: EV_WIDGET): BOOLEAN
-- Has v been inserted by the most recent insertion?
-- (By default, the value returned is equivalent to calling
-- `has (v)'. However, descendants might be able to provide more
-- efficient implementations.)
-- (from COLLECTION)

is_maximized: BOOLEAN
-- Is displayed at maximum size?
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_TITLED_WINDOW
bridge_ok: Result = implementation.is_maximized

is_minimized: BOOLEAN
-- Is displayed iconified/minimised?
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_TITLED_WINDOW
bridge_ok: Result = implementation.is_minimized

is_modal: BOOLEAN
-- Must the window be closed before application can
-- receive user events again?
--
-- May be redefined in EV_DIALOG to return
-- a different value
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed

is_sensitive: BOOLEAN
-- Is object sensitive to user input.
-- (from EV_SENSITIVE)
require -- from EV_SENSITIVE
not_destroyed: not is_destroyed
ensure -- from EV_SENSITIVE
bridge_ok: Result = implementation.user_is_sensitive

is_show_requested: BOOLEAN
-- Will Current be displayed when its parent is?
-- See also is_displayed.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
bridge_ok: Result = implementation.is_show_requested

is_special (object: ANY): BOOLEAN
-- Is object a special object?
-- It only recognized a special object
-- initialized within a TO_SPECIAL object.
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

mode_is_drag_and_drop: BOOLEAN
-- Is the user interface mode drag and drop?
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_drag_and_drop

mode_is_pick_and_drop: BOOLEAN
-- Is the user interface mode pick and drop?
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_pick_and_drop

mode_is_target_menu: BOOLEAN
-- Is the user interface mode a pop-up menu of targets?
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then -- from EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_target_menu

prunable: BOOLEAN
-- May items be removed?
-- (from EV_CELL)

readable: BOOLEAN
-- Is there a current item that may be accessed?
-- (from EV_CELL)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed

user_can_resize: BOOLEAN
-- Can the user resize?
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
bridge_ok: Result = implementation.user_can_resize

writable: BOOLEAN
-- Is there a current item that may be modified?
-- (from EV_CELL)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed

feature -- Status setting

center_pointer
-- Position screen pointer over center of Current.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed

disable_capture
-- Disable grab of all user input events.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
not_has_capture: not has_capture

disable_pebble_positioning
-- Assign False to pebble_positioning_enabled.
-- The pick and drop will start at the pointer position.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure -- from EV_PICK_AND_DROPABLE
pebble_positioning_updated: not pebble_positioning_enabled

disable_sensitive
-- Make object non-sensitive to user input.
-- (from EV_SENSITIVE)
require -- from EV_SENSITIVE
not_destroyed: not is_destroyed
ensure -- from EV_SENSITIVE
is_unsensitive: not is_sensitive

disable_user_resize
-- Prevent user from resizing.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
not_user_can_resize: not user_can_resize

enable_capture
-- Grab all user input events (mouse and keyboard).
-- disable_capture must be called to resume normal input handling.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
is_displayed: is_displayed
ensure -- from EV_WIDGET
has_capture: has_capture

enable_pebble_positioning
-- Assign True to pebble_positioning_enabled.
-- Use pebble_x_position and pebble_y_position as the initial coordinates
-- for the pick and drop in pixels relative to Current.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure -- from EV_PICK_AND_DROPABLE
pebble_positioning_updated: pebble_positioning_enabled

enable_sensitive
-- Make object sensitive to user input.
-- (from EV_SENSITIVE)
require -- from EV_SENSITIVE
not_destroyed: not is_destroyed
ensure -- from EV_SENSITIVE
is_sensitive: (parent = void or parent_is_sensitive) implies is_sensitive

enable_user_resize
-- Allow user to resize.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
user_can_resize: user_can_resize

hide
-- Request that Current not be displayed even when its parent is.
-- Make is_show_requested False.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
not_is_show_requested: not is_show_requested

lock_update
-- Lock drawing updates for this window on certain platforms until
-- unlock_update is called.
--
-- Note: - Only one window can be locked at a time.
-- - The window cannot be moved while update is locked.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
no_locked_window: ((create {EV_ENVIRONMENT}).application.locked_window = void)
ensure -- from EV_WINDOW
locked_window_is_current: (create {EV_ENVIRONMENT}).application.locked_window = Current

lower
-- Request that window be displayed below all other windows.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed

maximize
-- Display at maximum size.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_TITLED_WINDOW
is_maximized: is_maximized

merge_radio_button_groups (other: EV_CONTAINER)
-- Merge Current radio button group with that of other.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
other_not_void: other /= void

minimize
-- Display iconified/minimised.
-- It is not possible to guarantee this on some
-- platform configurations.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed

raise
-- Request that window be displayed above all other windows.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed

remove_menu_bar
-- Make menu_bar Void.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
void: menu_bar = void

remove_pebble
-- Make pebble Void and pebble_function `Void,
-- Removing transport.
-- (from EV_PICK_AND_DROPABLE)
ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
pebble_removed: pebble = void and pebble_function = void

remove_title
-- Make title Void.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_WINDOW
a_title_removed: title = void

restore
-- Restore to original position when minimized or maximized.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_TITLED_WINDOW
minimize_restored: old is_minimized implies not is_minimized
maximize_restored: old is_maximized implies not is_maximized

set_accept_cursor (a_cursor: EV_CURSOR)
-- Set a_cursor to be displayed when the screen pointer is over a
-- target that accepts pebble during pick and drop.
-- (from EV_PICK_AND_DROPABLE)
ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
accept_cursor_assigned: accept_cursor.is_equal (a_cursor)

set_actual_drop_target_agent (an_agent: like actual_drop_target_agent)
-- Assign an_agent to actual_drop_target_agent.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
an_agent_not_void: an_agent /= void
ensure -- from EV_WIDGET
assigned: actual_drop_target_agent = an_agent

set_default_colors
-- Set foreground and background color to their default values.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
not_destroyed: not is_destroyed

set_deny_cursor (a_cursor: EV_CURSOR)
-- Set a_cursor to be displayed when the screen pointer is not
-- over a valid target.
-- (from EV_PICK_AND_DROPABLE)
ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
deny_cursor_assigned: deny_cursor.is_equal (a_cursor)

set_drag_and_drop_mode
-- Set user interface mode to drag and drop.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure -- from EV_PICK_AND_DROPABLE
drag_and_drop_set: mode_is_drag_and_drop

set_focus
-- Grab keyboard focus.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
is_displayed: is_displayed
is_sensitive: is_sensitive
ensure -- from EV_WIDGET
has_focus: has_focus

set_height (a_height: INTEGER)
-- Assign a_height to height in pixels.
-- (from EV_POSITIONABLE)
require -- from EV_POSITIONABLE
a_height_positive_or_zero: a_height >= 0
ensure -- from EV_POSITIONABLE
height_assigned: height = minimum_height or else height = a_height

set_maximum_height (a_maximum_height: INTEGER)
-- Assign a_maximum_height to maximum_height in pixels.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
a_maximum_height_non_negative: a_maximum_height >= 0
a_maximum_height_not_less_than_minimum_height: a_maximum_height >= minimum_height
ensure -- from EV_WINDOW
maximum_height_assigned: maximum_height = a_maximum_height

set_maximum_size (a_maximum_width, a_maximum_height: INTEGER)
-- Assign a_maximum_width to maximum_width
-- and a_maximum_height to maximum_height in pixels.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
a_maximum_width_not_less_than_minimum_width: a_maximum_width >= minimum_width
a_maximum_height_not_less_than_minimum_height: a_maximum_height >= minimum_height
ensure -- from EV_WINDOW
maximum_width_assigned: maximum_width = a_maximum_width
maximum_height_assigned: maximum_height = a_maximum_height

set_maximum_width (a_maximum_width: INTEGER)
-- Assign a_maximum_width to maximum_width in pixels.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
a_maximum_width_non_negative: a_maximum_width >= 0
a_maximum_width_not_less_than_minimum_width: a_maximum_width >= minimum_width
ensure -- from EV_WINDOW
maximum_width_assigned: maximum_width = a_maximum_width

set_menu_bar (a_menu_bar: EV_MENU_BAR)
-- Assign a_menu_bar to menu_bar.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
no_menu_bar_assigned: menu_bar = void
a_menu_bar_not_void: a_menu_bar /= void
ensure -- from EV_WINDOW
assigned: menu_bar = a_menu_bar

set_pebble (a_pebble: like pebble)
-- Assign a_pebble to pebble.
-- Overrides set_pebble_function.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_ABSTRACT_PICK_AND_DROPABLE
a_pebble_not_void: a_pebble /= void
ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
pebble_assigned: pebble = a_pebble

set_pebble_function (a_function: FUNCTION [ANY, TUPLE, ANY])
-- Set a_function to compute pebble.
-- It will be called once each time a pick occurs, the result
-- will be assigned to pebble for the duration of transport.
-- When a pick occurs, the pick position in widget coordinates,
-- <<x, y>> in pixels, is passed.
-- To handle this data use a_function of type
-- FUNCTION [ANY, TUPLE [INTEGER, INTEGER], ANY] and return the
-- pebble as a function of x and y.
-- Overrides set_pebble.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_ABSTRACT_PICK_AND_DROPABLE
a_function_not_void: a_function /= void
a_function_takes_two_integer_open_operands: a_function.valid_operands ([1, 1])
ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
pebble_function_assigned: pebble_function = a_function

set_pebble_position (a_x, a_y: INTEGER)
-- Set the initial position for pick and drop
-- Coordinates are in pixels and are relative to position of Current.
-- Pebble_positioning_enabled must be True for the position to be used,
-- use enable_pebble_positioning.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure -- from EV_PICK_AND_DROPABLE
pebble_position_assigned: pebble_x_position = a_x and pebble_y_position = a_y

set_pick_and_drop_mode
-- Set user interface mode to pick and drop.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure -- from EV_PICK_AND_DROPABLE
pick_and_drop_set: mode_is_pick_and_drop

set_position (a_x, a_y: INTEGER)
-- Assign a_x to x_position and a_y to y_position in pixels.
-- (from EV_POSITIONABLE)
ensure -- from EV_POSITIONABLE
x_position_assigned: x_position = a_x
y_position_assigned: y_position = a_y

set_size (a_width, a_height: INTEGER)
-- Assign a_width to width and a_height to height in pixels.
-- (from EV_POSITIONABLE)
require -- from EV_POSITIONABLE
a_width_positive_or_zero: a_width >= 0
a_height_positive_or_zero: a_height >= 0
ensure -- from EV_POSITIONABLE
width_assigned: width = minimum_width or else width = a_width
height_assigned: height = minimum_height or else height = a_height

set_target_menu_mode
-- Set user interface mode to pop-up menu of targets.
-- (from EV_PICK_AND_DROPABLE)
require -- from EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure -- from EV_PICK_AND_DROPABLE
target_menu_mode_set: mode_is_target_menu

set_target_name (a_name: STRING)
-- Assign a_name to target_name.
-- (from EV_ABSTRACT_PICK_AND_DROPABLE)
require -- from EV_ABSTRACT_PICK_AND_DROPABLE
a_name_not_void: a_name /= void
ensure -- from EV_ABSTRACT_PICK_AND_DROPABLE
target_name_assigned: a_name /= target_name and a_name.is_equal (target_name)

set_title (a_title: STRING)
-- Assign a_title to title.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
a_title_not_void: a_title /= void
a_title_not_empty: not a_title.is_empty
ensure -- from EV_WINDOW
a_title_assigned: title.is_equal (a_title)

set_width (a_width: INTEGER)
-- Assign a_width to width in pixels.
-- (from EV_POSITIONABLE)
require -- from EV_POSITIONABLE
a_width_positive_or_zero: a_width >= 0
ensure -- from EV_POSITIONABLE
width_assigned: width = minimum_width or else width = a_width

set_x_position (a_x: INTEGER)
-- Assign a_x to x_position in pixels.
-- (from EV_POSITIONABLE)
ensure -- from EV_POSITIONABLE
x_position_assigned: x_position = a_x

set_y_position (a_y: INTEGER)
-- Assign a_y to y_position in pixels.
-- (from EV_POSITIONABLE)
ensure -- from EV_POSITIONABLE
y_position_assigned: y_position = a_y

show
-- Request that Current be displayed when its parent is.
-- True by default.
-- Make is_show_requested True.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
ensure -- from EV_WIDGET
is_show_requested: is_show_requested

unlock_update
-- Unlock updates for this widget on certain platforms.
-- (from EV_WINDOW)
require -- from EV_WINDOW
not_destroyed: not is_destroyed
locked_window_is_current: (create {EV_ENVIRONMENT}).application.locked_window = Current
ensure -- from EV_WINDOW
no_locked_window: ((create {EV_ENVIRONMENT}).application.locked_window = void)

feature -- Element change

extend (v: like item)
-- Ensure that structure includes v.
-- Do not move cursor.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
extendible: extendible
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: v /= Current
v_not_parent_of_current: not is_parent_recursive (v)
v_not_window: not v.conforms_to (create {EV_WINDOW})
ensure -- from EV_CONTAINER
has_v: has (v)

fill (other: CONTAINER [EV_WIDGET])
-- Fill with as many items of other as possible.
-- The representations of other and current structure
-- need not be the same.
-- (from COLLECTION)
require -- from COLLECTION
other_not_void: other /= void
extendible

put (v: like item)
-- Replace item with v.
-- Was declared in EV_CONTAINER as synonym of replace.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
writable: writable
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: v /= Current
v_not_parent_of_current: not is_parent_recursive (v)
v_not_window: not v.conforms_to (create {EV_WINDOW})
ensure -- from EV_CONTAINER
has_v: has (v)

remove_help_context
-- Remove key press action associated with EV_APPLICATION.help_key.
-- (from EV_HELP_CONTEXTABLE)
require -- from EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
help_context_not_void: help_context /= void
ensure -- from EV_HELP_CONTEXTABLE
no_help_context: help_context = void

remove_icon_name
-- Make icon_name Void.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
ensure -- from EV_TITLED_WINDOW
icon_name_removed: icon_name = void

replace (v: like item)
-- Replace item with v.
-- Was declared in EV_CONTAINER as synonym of put.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
writable: writable
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: v /= Current
v_not_parent_of_current: not is_parent_recursive (v)
v_not_window: not v.conforms_to (create {EV_WINDOW})
ensure -- from EV_CONTAINER
has_v: has (v)

set_background_color (a_color: like background_color)
-- Assign a_color to foreground_color.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
not_destroyed: not is_destroyed
a_color_not_void: a_color /= void
ensure -- from EV_COLORIZABLE
background_color_assigned: background_color.is_equal (a_color)

set_boolean_field (i: INTEGER; object: ANY; value: BOOLEAN)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
boolean_field: field_type (i, object) = boolean_type

set_character_field (i: INTEGER; object: ANY; value: CHARACTER)
-- Set character value of i-th field of object to value
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
character_field: field_type (i, object) = character_type

set_data (some_data: like data)
-- Assign some_data to data.
-- (from EV_ANY)
require -- from EV_ANY
not_destroyed: not is_destroyed
ensure -- from EV_ANY
data_assigned: data = some_data

set_double_field (i: INTEGER; object: ANY; value: DOUBLE)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
double_field: field_type (i, object) = double_type

set_foreground_color (a_color: like foreground_color)
-- Assign a_color to foreground_color.
-- (from EV_COLORIZABLE)
require -- from EV_COLORIZABLE
not_destroyed: not is_destroyed
a_color_not_void: a_color /= void
ensure -- from EV_COLORIZABLE
foreground_color_assigned: foreground_color.is_equal (a_color)

set_help_context (an_help_context: like help_context)
-- Assign an_help_context to help_context.
-- (from EV_HELP_CONTEXTABLE)
require -- from EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
an_help_context_not_void: an_help_context /= void
ensure -- from EV_HELP_CONTEXTABLE
help_context_assigned: help_context.is_equal (an_help_context)

set_icon_name (an_icon_name: STRING)
-- Assign an_icon_name to icon_name.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
an_icon_name_not_void: an_icon_name /= void
an_icon_name_not_empty: not an_icon_name.is_empty
ensure -- from EV_TITLED_WINDOW
icon_name_assigned: icon_name.is_equal (an_icon_name)

set_icon_pixmap (an_icon: EV_PIXMAP)
-- Assign an_icon to icon.
-- (from EV_TITLED_WINDOW)
require -- from EV_TITLED_WINDOW
not_destroyed: not is_destroyed
pixmap_not_void: an_icon /= void
ensure -- from EV_TITLED_WINDOW
icon_pixmap_assigned: icon_pixmap.is_equal (an_icon)

set_integer_field (i: INTEGER; object: ANY; value: INTEGER)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
integer_field: field_type (i, object) = integer_type

set_minimum_height (a_minimum_height: INTEGER)
-- Set a_minimum_height in pixels to minimum_height.
-- If height is less than a_minimim_height, resize.
-- This setting takes effect next time application is idle.
-- From now, minimum_height is fixed and will not be changed
-- dynamically by the application anymore.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_height_positive: a_minimum_height > 0
ensure -- from EV_WIDGET
minimum_height_assigned: minimum_height = a_minimum_height

set_minimum_size (a_minimum_width, a_minimum_height: INTEGER)
-- Assign a_minimum_height to minimum_height
-- and a_minimum_width to minimum_width in pixels.
-- If width or height is less than minimum size, resize.
-- This setting takes effect next time application is idle.
-- From now, minimum size is fixed and will not be changed
-- dynamically by the application anymore.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_width_positive: a_minimum_width > 0
a_minimum_height_positive: a_minimum_height > 0
ensure -- from EV_WIDGET
minimum_width_assigned: minimum_width = a_minimum_width
minimum_height_assigned: minimum_height = a_minimum_height

set_minimum_width (a_minimum_width: INTEGER)
-- Assign a_minimum_width in pixels to minimum_width.
-- If width is less than a_minimim_width, resize.
-- This setting takes effect next time application is idle.
-- From now, minimum_width is fixed and will not be changed
-- dynamically by the application anymore.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
a_minimum_width_positive: a_minimum_width > 0
ensure -- from EV_WIDGET
minimum_width_assigned: minimum_width = a_minimum_width

set_pointer_field (i: INTEGER; object: ANY; value: POINTER)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
pointer_field: field_type (i, object) = pointer_type

set_pointer_style (a_cursor: like pointer_style)
-- Assign a_cursor to pointer_style.
-- (from EV_WIDGET)
require -- from EV_WIDGET
not_destroyed: not is_destroyed
a_cursor_not_void: a_cursor /= void
ensure -- from EV_WIDGET
pointer_style_assigned: pointer_style.is_equal (a_cursor)

set_real_field (i: INTEGER; object: ANY; value: REAL)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
real_field: field_type (i, object) = real_type

set_reference_field (i: INTEGER; object: ANY; value: ANY)
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void
index_large_enough: i >= 1
index_small_enough: i <= field_count (object)
reference_field: field_type (i, object) = reference_type

feature -- Removal

prune (v: EV_WIDGET)
-- Remove v if contained.
-- (from EV_CELL)
require -- from COLLECTION
prunable: prunable
ensure then -- from EV_CELL
not has (v)

prune_all (v: EV_WIDGET)
-- Remove all occurrences of v.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from COLLECTION)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
no_more_occurrences: not has (v)

wipe_out
-- Remove item.
-- (from EV_CELL)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: is_empty

feature -- Conversion

linear_representation: LINEAR [like item]
-- Representation as a linear structure
-- (from EV_CELL)

feature -- Duplication

copy (other: like Current)
-- Update current object using fields of object attached
-- to other, so as to yield equal objects.
-- (from EV_ANY)
require -- from ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure -- from ANY
is_equal: is_equal (other)

feature -- Basic operations

propagate_background_color
-- Propagate background_color to all children.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
ensure -- from EV_CONTAINER
background_color_propagated: background_color_propagated

propagate_foreground_color
-- Propagate foreground_color to all children.
-- (from EV_CONTAINER)
require -- from EV_CONTAINER
not_destroyed: not is_destroyed
ensure -- from EV_CONTAINER
foreground_color_propagated: foreground_color_propagated

feature -- Command

destroy
-- Destroy underlying native toolkit object.
-- Render Current unusable.
-- (from EV_ANY)
ensure -- from EV_ANY
is_destroyed: is_destroyed

feature -- Conformance

is_instance_of (object: ANY; type_id: INTEGER): BOOLEAN
-- Is object an instance of type type_id?
-- (from INTERNAL)
require -- from INTERNAL
object_not_void: object /= void

type_conforms_to (type1, type2: INTEGER): BOOLEAN
-- Does type1 conform to type2?
-- (from INTERNAL)

feature -- Creation

dynamic_type_from_string (class_type: STRING): INTEGER
-- Dynamic type corresponding to class_type.
-- If no dynamic type available, returns -1.
-- (from INTERNAL)
require -- from INTERNAL
class_type_not_void: class_type /= void
ensure -- from INTERNAL
valid_result: Result = - 1 or else Result >= 0

new_instance_of (type_id: INTEGER): ANY
-- New instance of dynamic type_id.
-- Note: returned object is not initialized and may
-- hence violate its invariant.
-- (from INTERNAL)

feature -- Event handling

close_request_actions: EV_NOTIFY_ACTION_SEQUENCE
-- Actions to be performed whan a request to close window
-- has been received.
-- (from EV_WINDOW_ACTION_SEQUENCES)
ensure -- from EV_WINDOW_ACTION_SEQUENCES
not_void: Result /= void

conforming_pick_actions: EV_NOTIFY_ACTION_SEQUENCE
-- Actions to be performed when a pebble that fits here is picked.
-- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES)
ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= void

drop_actions: EV_PND_ACTION_SEQUENCE
-- Actions to be performed when a pebble is dropped here.
-- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES)
ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= void

focus_in_actions: EV_FOCUS_ACTION_SEQUENCE
-- Actions to be performed when keyboard focus is gained.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

focus_out_actions: EV_FOCUS_ACTION_SEQUENCE
-- Actions to be performed when keyboard focus is lost.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

key_press_actions: EV_KEY_ACTION_SEQUENCE
-- Actions to be performed when a keyboard key is pressed.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

key_press_string_actions: EV_KEY_STRING_ACTION_SEQUENCE
-- Actions to be performed when a keyboard press generates a displayable character.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

key_release_actions: EV_KEY_ACTION_SEQUENCE
-- Actions to be performed when a keyboard key is released.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

move_actions: EV_GEOMETRY_ACTION_SEQUENCE
-- Actions to be performed when window moves.
-- (from EV_WINDOW_ACTION_SEQUENCES)
ensure -- from EV_WINDOW_ACTION_SEQUENCES
not_void: Result /= void

pick_actions: EV_PND_START_ACTION_SEQUENCE
-- Actions to be performed when pebble is picked up.
-- (from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES)
ensure -- from EV_PICK_AND_DROPABLE_ACTION_SEQUENCES
not_void: Result /= void

pointer_button_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
-- Actions to be performed when screen pointer button is pressed.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

pointer_button_release_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
-- Actions to be performed when screen pointer button is released.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

pointer_double_press_actions: EV_POINTER_BUTTON_ACTION_SEQUENCE
-- Actions to be performed when screen pointer is double clicked.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

pointer_enter_actions: EV_NOTIFY_ACTION_SEQUENCE
-- Actions to be performed when screen pointer enters widget.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

pointer_leave_actions: EV_NOTIFY_ACTION_SEQUENCE
-- Actions to be performed when screen pointer leaves widget.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

pointer_motion_actions: EV_POINTER_MOTION_ACTION_SEQUENCE
-- Actions to be performed when screen pointer moves.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

resize_actions: EV_GEOMETRY_ACTION_SEQUENCE
-- Actions to be performed when size changes.
-- (from EV_WIDGET_ACTION_SEQUENCES)
ensure -- from EV_WIDGET_ACTION_SEQUENCES
not_void: Result /= void

show_actions: EV_NOTIFY_ACTION_SEQUENCE
-- Actions to be performed when window is shown.
-- (from EV_WINDOW_ACTION_SEQUENCES)
ensure -- from EV_WINDOW_ACTION_SEQUENCES
not_void: Result /= void

feature -- Status Report

is_destroyed: BOOLEAN
-- Is Current no longer usable?
-- (from EV_ANY)
ensure -- from EV_ANY
bridge_ok: Result = implementation.is_destroyed

feature -- Version

compiler_version: INTEGER
-- (from INTERNAL)

invariant

-- from ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
-- from EV_TITLED_WINDOW
accelerators_not_void: is_usable implies accelerators /= void
-- from EV_WINDOW
consistent_horizontal_bounds: maximum_width >= minimum_width
consistent_vertical_bounds: maximum_height >= minimum_height
upper_bar_not_void: is_usable implies upper_bar /= void
lower_bar_not_void: is_usable implies lower_bar /= void
-- from EV_CONTAINER
client_width_within_bounds: is_usable implies client_width >= 0 and client_width <= width
client_height_within_bounds: is_usable implies client_height >= 0 and client_height <= height
all_radio_buttons_connected: is_usable implies all_radio_buttons_connected
parent_of_items_is_current: is_usable implies parent_of_items_is_current
items_unique: is_usable implies items_unique
-- from EV_WIDGET
pointer_position_not_void: is_usable and is_show_requested implies pointer_position /= void
is_displayed_implies_show_requested: is_usable and then is_displayed implies is_show_requested
parent_contains_current: is_usable and then parent /= void implies parent.has (Current)
-- from EV_PICK_AND_DROPABLE
user_interface_modes_mutually_exclusive: mode_is_pick_and_drop.to_integer + mode_is_drag_and_drop.to_integer + mode_is_target_menu.to_integer = 1
-- from EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= void and then implementation.interface = Current
default_create_called: default_create_called
-- from EV_COLORIZABLE
background_color_not_void: is_usable implies background_color /= void
foreground_color_not_void: is_usable implies foreground_color /= void
-- from EV_POSITIONED
width_not_negative: is_usable implies width >= 0
height_not_negative: is_usable implies height >= 0
minimum_width_not_negative: is_usable implies minimum_width >= 0
minimum_height_not_negative: is_usable implies minimum_height >= 0

end -- class MAIN_WINDOW