indexing
description: "Appearance of a screen pointer cursor, typically moved by a mouse."
legal: "See notice at end of class."
status: "See notice at end of class."
keywords: "mouse, pointer, cursor, arrow"
date: "$Date: 2006-12-06 10:59:06 -0800 (Wed, 06 Dec 2006) $"
revision: "$Revision: 65385 $"
class interface
EV_CURSOR
create
default_create
EV_ANY
require ANY
True
ensure then EV_ANY
is_coupled: implementation /= Void
is_initialized: is_initialized
default_create_called: default_create_called
is_in_default_state: is_in_default_state
make_with_size (a_width, a_height: INTEGER_32)
`a_width'`a_height'
EV_PIXMAP
require EV_PIXMAP
a_width_positive: a_width > 0
a_height_positive: a_height > 0
ensure then EV_PIXMAP
width_assigned: width = a_width
height_assigned: height = a_height
make_with_pixmap (a_pixmap: EV_PIXMAP; a_x_hotspot, a_y_hotspot: INTEGER_32)
`a_pixmap'
`a_x_hotspot'`a_y_hotspot'
make_with_pointer_style (a_pointer_style: EV_POINTER_STYLE)
`a_pointer_style'
convert
make_with_pointer_style ({EV_POINTER_STYLE})
feature
accept_cursor: EV_POINTER_STYLE
`Result'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_ABSTRACT_PICK_AND_DROPABLE
result_not_void: Result /= Void
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.accept_cursor
actual_drop_target_agent: FUNCTION [ANY, TUPLE [INTEGER_32, INTEGER_32], EV_ABSTRACT_PICK_AND_DROPABLE]
`Void'`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.actual_drop_target_agent
background_color: EV_COLOR
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.background_color)
clip_area: EV_RECTANGLE
EV_DRAWABLE
require EV_DRAWABLE
not_destroyed: not is_destroyed
ensure EV_DRAWABLE
bridge_ok: (Result = Void) = (implementation.clip_area = Void)
configurable_target_menu_handler: PROCEDURE [ANY, TUPLE [menu: EV_MENU; target_list: ARRAYED_LIST [EV_PND_TARGET_DATA]; source: EV_PICK_AND_DROPABLE; source_pebble: ANY]]
`Current'
EV_PICK_AND_DROPABLE
dashed_line_style: BOOLEAN
EV_DRAWABLE
require EV_DRAWABLE
not_destroyed: not is_destroyed
ensure EV_DRAWABLE
bridge_ok: Result = implementation.dashed_line_style
data: ANY
EV_ANY
default_identifier_name: STRING_8
EV_IDENTIFIABLE
ensure EV_IDENTIFIABLE
result_not_void: Result /= Void
result_not_empty: not Result.is_empty
no_period_in_result: not Result.has ('.')
default_key_processing_handler: PREDICATE [ANY, TUPLE [EV_KEY]] assign set_default_key_processing_handler
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.default_key_processing_handler
deny_cursor: EV_POINTER_STYLE
`Result'
pebble
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure EV_ABSTRACT_PICK_AND_DROPABLE
result_not_void: Result /= Void
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.deny_cursor
drawing_mode: INTEGER_32
EV_DRAWABLE
require EV_DRAWABLE
not_destroyed: not is_destroyed
ensure EV_DRAWABLE
bridge_ok: Result = implementation.drawing_mode
font: EV_FONT
`Current'
EV_FONTABLE
require EV_FONTABLE
not_destroyed: not is_destroyed
ensure EV_FONTABLE
not_void: Result /= Void
bridge_ok: Result.is_equal (implementation.font)
foreground_color: EV_COLOR
EV_COLORIZABLE
require EV_COLORIZABLE
not_destroyed: not is_destroyed
ensure EV_COLORIZABLE
bridge_ok: Result.is_equal (implementation.foreground_color)
full_identifier_path: STRING_8
EV_IDENTIFIABLE
ensure EV_IDENTIFIABLE
result_not_void: Result /= Void
result_correct: parent = Void implies Result.is_equal (identifier_name)
result_correct: parent /= Void implies Result.is_equal (parent.full_identifier_path + "." + identifier_name)
generating_type: STRING_8
ANY
ensure ANY
generating_type_not_void: Result /= Void
generating_type_not_empty: not Result.is_empty
generator: STRING_8
ANY
ensure ANY
generator_not_void: Result /= Void
generator_not_empty: not Result.is_empty
help_context: FUNCTION [ANY, TUPLE, EV_HELP_CONTEXT]
EV_HELP_CONTEXTABLE
require EV_HELP_CONTEXTABLE
not_destroyed: not is_destroyed
ensure EV_HELP_CONTEXTABLE
bridge_ok: Result = implementation.help_context
frozen id_object (an_id: INTEGER_32): ?IDENTIFIED
`an_id'
IDENTIFIED
ensure IDENTIFIED
consistent: Result = Void or else Result.object_id = an_id
identifier_name: STRING_8
default_identifier_name
EV_IDENTIFIABLE
ensure EV_IDENTIFIABLE
result_not_void: Result /= Void
result_not_empty: not Result.is_empty
no_period_in_result: not Result.has ('.')
default_name_available: not has_identifier_name_set implies Result.is_equal (default_identifier_name)
line_width: INTEGER_32
EV_DRAWABLE
require EV_DRAWABLE
not_destroyed: not is_destroyed
ensure EV_DRAWABLE
bridge_ok: Result = implementation.line_width
frozen object_id: INTEGER_32
IDENTIFIED
ensure IDENTIFIED
valid_id: Result > 0 implies id_object (Result) = Current
parent: EV_CONTAINER
`Current'
EV_WIDGET
require EV_IDENTIFIABLE
not_destroyed: not is_destroyed
ensure EV_IDENTIFIABLE
correct: has_parent implies Result /= Void
correct: not has_parent implies Result = Void
ensure then EV_WIDGET
bridge_ok: Result = implementation.parent
pebble: ANY
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble
pebble_function: FUNCTION [ANY, TUPLE, ANY]
EV_PICK_AND_DROPABLE
require EV_ABSTRACT_PICK_AND_DROPABLE
True
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_function
pebble_positioning_enabled: BOOLEAN
`True'
pebble_x_positionpebble_y_position
`False'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_positioning_enabled
pebble_x_position: INTEGER_32
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_x_position
pebble_y_position: INTEGER_32
`Current'
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.pebble_y_position
pointer_position: EV_COORDINATE
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
is_show_requested: is_show_requested
pointer_style: EV_POINTER_STYLE
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
real_target: EV_DOCKABLE_TARGET
`Result'
`Current'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.real_target
target_data_function: FUNCTION [ANY, TUPLE [ANY], EV_PND_TARGET_DATA]
EV_ABSTRACT_PICK_AND_DROPABLE
target_name: STRING_GENERAL
`Current'
EV_ABSTRACT_PICK_AND_DROPABLE
tile: EV_PIXMAP
foreground_color
EV_DRAWABLE
require EV_DRAWABLE
not_destroyed: not is_destroyed
ensure EV_DRAWABLE
bridge_ok: (Result = Void) = (implementation.tile = Void)
tooltip: STRING_32
`Current'
`Result'
EV_TOOLTIPABLE
require EV_TOOLTIPABLE
not_destroyed: not is_destroyed
ensure EV_TOOLTIPABLE
bridge_ok: is_bridge_ok (Result)
not_void: Result /= Void
cloned: is_cloned (Result)
x_hotspot: INTEGER_32
y_hotspot: INTEGER_32
feature
height: INTEGER_32
minimum_height
EV_POSITIONED
require EV_DRAWABLE
not_destroyed: not is_destroyed
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.height
minimum_height: INTEGER_32
height
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.minimum_height
positive_or_zero: Result >= 0
minimum_width: INTEGER_32
width
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.minimum_width
positive_or_zero: Result >= 0
screen_x: INTEGER_32
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.screen_x
screen_y: INTEGER_32
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.screen_y
width: INTEGER_32
minimum_width
EV_POSITIONED
require EV_DRAWABLE
not_destroyed: not is_destroyed
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.width
x_position: INTEGER_32
x_position
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.x_position
y_position: INTEGER_32
y_position
EV_POSITIONED
require EV_POSITIONED
not_destroyed: not is_destroyed
ensure EV_POSITIONED
bridge_ok: Result = implementation.y_position
feature
frozen deep_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies (other /= Void and then some.same_type (other))
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
frozen is_deep_equal (other: EV_CURSOR): BOOLEAN
`Current'`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
shallow_implies_deep: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_deep_equal (Current)
is_equal (other: EV_CURSOR): BOOLEAN
`other'`Current'
EV_PIXMAP
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
frozen standard_equal (some: ?ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: EV_CURSOR): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
has_capture: BOOLEAN
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.has_capture
has_focus: BOOLEAN
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.has_focus
has_identifier_name_set: BOOLEAN
EV_IDENTIFIABLE
has_parent: BOOLEAN
EV_IDENTIFIABLE
is_displayed: BOOLEAN
`Current'
`True'
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.is_displayed
is_dockable: BOOLEAN
`Current'
`True'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_dockable
is_external_docking_enabled: BOOLEAN
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_external_docking_enabled
is_external_docking_relative: BOOLEAN
`Current'
`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.is_external_docking_relative
is_sensitive: BOOLEAN
EV_SENSITIVE
require EV_SENSITIVE
not_destroyed: not is_destroyed
ensure EV_SENSITIVE
bridge_ok: Result = implementation.user_is_sensitive
is_show_requested: BOOLEAN
`Current'
is_displayed
EV_WIDGET
require EV_WIDGET
not_destroyed: not is_destroyed
ensure EV_WIDGET
bridge_ok: Result = implementation.is_show_requested
is_tabable_from: BOOLEAN
EV_TAB_CONTROLABLE
require EV_TAB_CONTROLABLE
not_destroyed: not is_destroyed
is_tabable_to: BOOLEAN
EV_TAB_CONTROLABLE
require EV_TAB_CONTROLABLE
not_destroyed: not is_destroyed
mode_is_configurable_target_menu: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_configurable_target_menu
mode_is_drag_and_drop: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_drag_and_drop
mode_is_pick_and_drop: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_pick_and_drop
mode_is_target_menu: BOOLEAN
EV_PICK_AND_DROPABLE
require EV_PICK_AND_DROPABLE
not_destroyed: not is_destroyed
ensure then EV_PICK_AND_DROPABLE
bridge_ok: Result = implementation.mode_is_target_menu
real_source: EV_DOCKABLE_SOURCE
`Result'
`Current'
`Void'`Current'
EV_DOCKABLE_SOURCE
require EV_DOCKABLE_SOURCE
not_destroyed: not is_destroyed
ensure EV_DOCKABLE_SOURCE
bridge_ok: Result = implementation.real_source
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
feature