indexing
description: "Contains information about the size and position of a window."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
WEL_WINDOW_POS
create
make
item
WEL_STRUCTURE
ensure WEL_STRUCTURE
not_shared: not shared
make_by_pointer (a_pointer: POINTER)
itema_pointer
item
a_pointer
WEL_ANY
ensure WEL_ANY
item_set: item = a_pointer
shared: shared
feature
flags: INTEGER
WEL_SWP_CONSTANTS
ensure
positive_result: Result >= 0
height: INTEGER
ensure
positive_result: Result >= 0
hwindow_insert_after: POINTER
item: POINTER
WEL_ANY
width: INTEGER
ensure
positive_result: Result >= 0
window: WEL_WINDOW
window_insert_after: WEL_WINDOW
x: INTEGER
y: INTEGER
feature
structure_size: INTEGER
ensure WEL_STRUCTURE
positive_result: Result > 0
feature
exists: BOOLEAN
item
WEL_ANY
ensure WEL_ANY
Result = (item /= default_pointer)
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
feature
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
feature
set_bottom
window
set_flags (a_flags: INTEGER)
flagsa_flags
WEL_SWP_CONSTANTSa_flags
ensure
flags_set: flags = a_flags
set_height (a_height: INTEGER)
heighta_height
ensure
height_set: height = a_height
set_hwindow_insert_after (a_window: POINTER)
window_insert_aftera_window
set_item (an_item: POINTER)
iteman_item
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
set_no_topmost
set_top
set_topmost
set_width (a_width: INTEGER)
widtha_width
ensure
width_set: width = a_width
set_window (a_window: WEL_WINDOW)
windowa_window
require
a_window_not_void: a_window /= void
a_window_exists: a_window.exists
ensure
window_set: window = a_window
set_window_insert_after (a_window: WEL_WINDOW)
window_insert_aftera_window
require
a_window_not_void: a_window /= void
a_window_exists: a_window.exists
ensure
window_insert_after_set: window_insert_after = a_window
set_x (a_x: INTEGER)
xa_x
ensure
x_set: x = a_x
set_y (a_y: INTEGER)
ya_y
ensure
y_set: y = a_y
feature
dispose
Current
Current
WEL_ANY
feature
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
feature
initialize
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
initialize_with_character (a_character: CHARACTER)
a_character
WEL_STRUCTURE
require WEL_STRUCTURE
exists: exists
memory_copy (source_pointer: POINTER; length: INTEGER)
lengthsource_pointeritem
WEL_STRUCTURE
require WEL_STRUCTURE
length_small_enough: length <= structure_size
length_large_enough: length > 0
exists: exists
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_WINDOW_POS