indexing
description: "Small picture whose location on the screen is controlled by a pointing device."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
WEL_CURSOR
create
make_by_id (id: INTEGER)
id
WEL_GRAPHICAL_RESOURCE
require WEL_RESOURCE
valid_id: id > 0
ensure WEL_RESOURCE
not_shared: not shared
make_by_name (name: STRING)
name
WEL_GRAPHICAL_RESOURCE
require WEL_RESOURCE
name_not_void: name /= void
name_not_empty: not name.is_empty
ensure WEL_RESOURCE
not_shared: not shared
make_by_file (file_name: STRING)
file_name
WEL_GRAPHICAL_RESOURCE
require WEL_GRAPHICAL_RESOURCE
file_name_not_void: file_name /= void
make_by_bitmask (x_hot_spot, y_hot_spot: INTEGER; and_plane, xor_plane: ARRAY [CHARACTER])
and_planexor_plane
x_hot_spoty_hot_spot
require
x_hot_spot_large_enough: x_hot_spot >= 0
x_hot_spot_small_enough: x_hot_spot < cursor_width
y_hot_spot_large_enough: y_hot_spot >= 0
y_hot_spot_small_enough: y_hot_spot < cursor_height
and_plane_not_void: and_plane /= void
xor_plane_not_void: xor_plane /= void
and_plane_not_empty: not and_plane.is_empty
xor_plane_not_empty: not xor_plane.is_empty
make_by_predefined_id (id: POINTER)
id
WEL_GRAPHICAL_RESOURCE
ensure WEL_RESOURCE
shared: shared
make_by_pointer (a_pointer: POINTER)
itema_pointer
item
a_pointer
WEL_GDI_ANY
ensure WEL_ANY
item_set: item = a_pointer
shared: shared
make_by_icon_info (icon_info: WEL_ICON_INFO)
icon_info
WEL_GRAPHICAL_RESOURCE
ensure WEL_GRAPHICAL_RESOURCE
item_not_void: item /= void
feature
gdi_objects_count: INTEGER
WEL_GDI_ANY
get_icon_info: WEL_ICON_INFO
WEL_GRAPHICAL_RESOURCE
ensure WEL_GRAPHICAL_RESOURCE
result_void_or_valid: Result = void or else Result.is_initialized
item: POINTER
WEL_ANY
previous_cursor: WEL_CURSOR
x_hotspot: INTEGER
Current
y_hotspot: INTEGER
Current
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_item (an_item: POINTER)
iteman_item
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
feature
delete
WEL_GRAPHICAL_RESOURCE
require WEL_REFERENCE_TRACKABLE
reference_not_tracked: not reference_tracked
ensure WEL_REFERENCE_TRACKABLE
destroyed: not shared implies not exists
delete_gdi_object
WEL_GRAPHICAL_RESOURCE
ensure WEL_GDI_ANY
not_exists: not exists
dispose
Current
delete
WEL_REFERENCE_TRACKABLE
feature
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
feature
restore_previous
previous_cursor
require
previous_cursor_not_void: previous_cursor /= void
ensure
previous_cursor_void: previous_cursor = void
set
previous_cursor
require
exists: exists
feature
reference_tracked: BOOLEAN
Current
WEL_REFERENCE_TRACKABLE
references_count: INTEGER
WEL_REFERENCE_TRACKABLE
feature
decrement_reference
delete
WEL_REFERENCE_TRACKABLE
require WEL_REFERENCE_TRACKABLE
exists: exists
tracking_references_started: reference_tracked
enable_reference_tracking
references_tracked
WEL_REFERENCE_TRACKABLE
require WEL_REFERENCE_TRACKABLE
exists: exists
tracking_reference_not_started: not reference_tracked
increment_reference
WEL_REFERENCE_TRACKABLE
require WEL_REFERENCE_TRACKABLE
exists: exists
tracking_references_started: reference_tracked
object_id: INTEGER
Current
WEL_REFERENCE_TRACKABLE
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_CURSOR