Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

em.widget.widgets

Class EM_BUTTON


Direct ancestors

EM_WIDGET

Creation

Features

Invariants

indexing

description

A push button with a label and/or an image.

Events:
- clicked_event: Triggered when clicked. Passes no arguments.

date

$Date: 2005/10/23 11:24:49 $

revision

$Revision: 1.20 $

class

EM_BUTTON

inherit

EM_WIDGET

create

make_void_surface

-- Initialise default values.

-- (From EM_2D_COMPONENT)

ensure
surface_void: surface = Void
make_from_dimension (a_width: like width; a_height: like height)

-- Initialise Current with dimensions a_width a_height.

-- (From EM_2D_COMPONENT)

ensure
surface_created: surface /= Void
width_set: width = a_width
height_set: height = a_height
make_from_text (a_text: like text)

-- Initialise Current with a_text as label.

require
a_text_not_void: a_text /= Void
ensure
text_set: text = a_text
make_from_image (an_image: like image)

-- Initialise Current with an_image as image.

require
an_image_not_void: an_image /= Void
ensure
image_set: image = an_image
make_from_text_image (a_text: like text; an_image: like image)

-- Initialise Current with a_text as label and an_image as image.

require
an_image_not_void: an_image /= Void
ensure
text_set: text = a_text
image_set: image = an_image
make_empty

-- Initialise Current with empty text

feature -- Access

background: EM_BACKGROUND

-- Background of widget

-- (From EM_WIDGET)

border: EM_BORDER

-- Border of widget

-- (From EM_WIDGET)

delegate: EM_WIDGET_DELEGATE

-- Delegate which draws widget

-- (From EM_WIDGET)

disabled_image: EM_BITMAP

-- Disabled image on Current

font: EM_FONT

-- Font of widget

-- (From EM_WIDGET)

foreground_color: EM_COLOR

-- Foreground color of widget

-- (From EM_WIDGET)

image: EM_BITMAP

-- Image on Current

screen_x: INTEGER

-- X position of Current on screen

-- (From EM_WIDGET)

screen_y: INTEGER

-- Y position of Current on screen

-- (From EM_WIDGET)

surface: EM_SURFACE

-- Surface to draw on

-- (From EM_2D_COMPONENT)

text: STRING

-- Text on Current

tooltip: STRING

-- Tooltip of Current

-- (From EM_COMPONENT)

widgets: DS_LINEAR [EM_WIDGET]

-- Nested widgets.

-- (From EM_WIDGET)

ensure
widgets_not_void: Result /= Void
x: INTEGER

-- X position of Current relative to parent

-- (From EM_COMPONENT)

y: INTEGER

-- Y position of Current relative to parent

-- (From EM_COMPONENT)

feature -- Measurement

height: INTEGER

-- Height of Current

-- (From EM_COMPONENT)

inner_height: INTEGER

-- Inner height of Current

-- (From EM_WIDGET)

ensure
height_minus_border: Result = height - border.top - border.bottom
inner_width: INTEGER

-- Inner width of Current

-- (From EM_WIDGET)

ensure
width_minus_border: Result = width - border.left - border.right
optimal_height: INTEGER

-- Optimal height of Current

-- (From EM_WIDGET)

optimal_width: INTEGER

-- Optimal width of Current

-- (From EM_WIDGET)

width: INTEGER

-- Width of Current

-- (From EM_COMPONENT)

feature -- Status report

has_widget (a_widget: EM_WIDGET): BOOLEAN

--Is a_widget present on this widget?

-- (From EM_WIDGET)

require
a_widget_not_void: a_widget /= Void
is_changed: BOOLEAN

-- Is this widget changed since last draw?

-- (From EM_WIDGET)

is_enabled: BOOLEAN

-- Is Current enabled?

-- (From EM_COMPONENT)

is_joystick_sensitive: BOOLEAN

-- Does Current handle joystick events?

-- (From EM_INPUT_SENSITIVE)

is_keyboard_sensitive: BOOLEAN

-- Does Current handle keyboard events?

-- (From EM_INPUT_SENSITIVE)

is_mouse_over: BOOLEAN

-- Is mouse over Current?

is_mouse_sensitive: BOOLEAN

-- Does Current handle mouse events?

-- (From EM_INPUT_SENSITIVE)

is_pressed: BOOLEAN

-- Is mouse down on Current?

is_visible: BOOLEAN

-- Is Current visible?

-- (From EM_COMPONENT)

feature -- Status setting

disable

-- Disable button.

-- (From EM_COMPONENT)

ensure
not_enabled: not is_enabled
ensure then
is_changed: is_changed
enable

-- Enable button.

-- (From EM_COMPONENT)

ensure
enabled: is_enabled
ensure then
is_changed: is_changed
hide

-- Hide Current.
-- This will trigger a hide event.

-- (From EM_COMPONENT)

ensure
not_visible: not is_visible
set_changed

-- Set this widget's changed status to true.
-- This also sets the changed status of the parent widget (if any) to true.

-- (From EM_WIDGET)

ensure
is_changed: is_changed
set_enabled (a_value: like is_enabled)

-- Set is_enabled to a_value.

-- (From EM_COMPONENT)

ensure
is_enabled_set: is_enabled = a_value
set_joystick_sensitive (sensitive: BOOLEAN)

-- Set joystick sensitivity status.

-- (From EM_INPUT_SENSITIVE)

ensure
joystick_sensitivity_set: is_joystick_sensitive = sensitive
set_keyboard_sensitive (sensitive: BOOLEAN)

-- Set keyboard sensitivity status.

-- (From EM_INPUT_SENSITIVE)

ensure
keyboard_sensitivity_set: is_keyboard_sensitive = sensitive
set_mouse_over (value: BOOLEAN)

-- Set is_mouse_over to value.

ensure
is_mouse_over_set: is_mouse_over = value
changed: is_changed
set_mouse_sensitive (sensitive: BOOLEAN)

-- Set mouse sensitivity status.

-- (From EM_INPUT_SENSITIVE)

ensure
mouse_sensitivity_set: is_mouse_sensitive = sensitive
set_pressed (value: BOOLEAN)

-- Set is_pressed to value.

ensure
is_pressed_set: is_pressed = value
changed: is_changed
set_unchanged

-- Set widget's changed status to false.

-- (From EM_WIDGET)

ensure
not_changed: not is_changed
show

-- Show Current.
-- This will trigger a show event.

-- (From EM_COMPONENT)

ensure
visible: is_visible

feature -- Element change

add_widget (a_widget: EM_WIDGET)

-- Add a_widget to nested widgets.

-- (From EM_WIDGET)

require
a_widget_not_void: a_widget /= Void
a_widget_not_present: not widgets.has (a_widget)
a_widget_not_current: a_widget /= Current
ensure
a_widget_added: widgets.has (a_widget)
a_widgets_parent_set: a_widget.parent_widget = Current
changed: is_changed
resize_to_optimal_dimension

-- Set dimension to optimal_width optimal_height.

-- (From EM_WIDGET)

ensure
width_set: width = optimal_width
height_set: height = optimal_height
changed: is_changed
set_background (a_background: like background)

-- Set background to a_background.

-- (From EM_WIDGET)

ensure
background_set: background = a_background
changed: is_changed
set_background_color (a_color: EM_COLOR)

-- Set background to display a_color as color.
-- If a_color has an alpha value of 255, an EM_COLOR_BACKGROUND will be used.
-- Otherwise an EM_ALPHA_COLOR_BACKGROUND or an
-- EM_TRANSPARENT_BACKGROUND is used.

-- (From EM_WIDGET)

require
a_color_not_void: a_color /= Void
ensure
background_set: background /= Void
changed: is_changed
set_border (a_border: like border)

-- Set border to a_border.
-- To clear the border, pass 'Void'.

-- (From EM_WIDGET)

ensure
border_set: a_border /= Void implies border = a_border
border_empty: a_border = Void implies border = No_border
changed: is_changed
set_delegate (a_delegate: like delegate)

-- Set delegate to a_delegate.

-- (From EM_WIDGET)

ensure
delegate_set: delegate = a_delegate
set_disabled_image (an_image: like disabled_image)

-- Set disabled_image to an_image.

ensure
image_set: disabled_image = an_image
set_font (a_font: like font)

-- Set font to a_font.

-- (From EM_WIDGET)

require
a_font_not_void: a_font /= Void
ensure
font_set: font = a_font
changed: is_changed
set_foreground_color (a_color: like foreground_color)

-- Set foreground_color to a_color.

-- (From EM_WIDGET)

require
a_color_not_void: a_color /= Void
ensure
foreground_color_set: foreground_color = a_color
changed: is_changed
set_image (an_image: like image)

-- Set image to an_image.

require
an_image_not_void: an_image /= Void
ensure
image_set: image = an_image
set_optimal_dimension (a_width: like optimal_width; a_height: like optimal_height)

-- Set optimal dimension to a_width a_height.
-- The dimenson of the widget will not change, but subsequent calls to optimal_width
-- and optimal_height will return a_width and a_height. Also a call to resize_to_optimal_dimension
-- will set the widget's dimension to a_width a_height.
-- This setting will overwrite the optimal dimension definded by the widget delegate.
-- If a negative width or height is set, the optimal dimension will be set by the
-- delegate again.

-- (From EM_WIDGET)

ensure
optimal_width_set: a_width >= 0 implies optimal_width = a_width
optimal_height_set: a_height >= 0 implies optimal_height = a_height
set_position (a_x: like x; a_y: like y)

-- Set position to a_x a_y.
-- This will trigger a move event.

-- (From EM_COMPONENT)

ensure
x_set: x = a_x
y_set: y = a_y
set_text (a_text: like text)

-- Set text to a_text.

require
a_text_not_void: a_text /= Void
ensure
text_set: text = a_text
changed: is_changed
set_tooltip (a_tooltip: like tooltip)

-- Set tooltip to a_tooltip.

-- (From EM_COMPONENT)

ensure
tooltip_set: tooltip = a_tooltip
set_transparent
ensure
background_set: background /= Void
changed: is_changed
set_transparent_color (a_color: EM_COLOR)

-- Set background to be transparent and use a_color as transparent colorkey (this color will be 100% transparent).
-- This sets the background to a EM_COLOR_BACKGROUND using a_color as color and
-- also sets the transparent colorkey of the surface to a_color

-- (From EM_WIDGET)

ensure
surface_colorkey_set: surface.has_transparent_colorkey
changed: is_changed
set_x (a_x: like x)

-- Set x to a_x.

-- (From EM_COMPONENT)

ensure
x_set: x = a_x
set_y (a_y: like y)

-- Set y to a_y.

-- (From EM_COMPONENT)

ensure
y_set: y = a_y

feature -- Removal

remove_widget (a_widget: EM_WIDGET)

-- Remove a_widget from nested widgets.

-- (From EM_WIDGET)

require
a_widget_not_void: a_widget /= Void
ensure
a_widget_removed: not widgets.has (a_widget)
a_widgets_parent_set: a_widget.parent_widget = Void
changed: is_changed

feature -- Resizing

set_dimension (a_width: like width; a_height: like height)

-- Set dimension to a_width a_height.
-- This will trigger a resize event.

-- (From EM_COMPONENT)

require
a_width_not_negative: a_width >= 0
a_height_not_negative: a_height >= 0
ensure
width_set: width = a_width
height_set: height = a_height
set_height (a_height: like height)

-- Set height to a_height.

-- (From EM_COMPONENT)

require
a_height_not_negative: a_height >= 0
ensure
height_set: height = a_height
set_width (a_width: like width)

-- Set width to a_width.

-- (From EM_COMPONENT)

require
a_width_not_negative: a_width >= 0
ensure
width_set: width = a_width

feature -- Miscellaneous

next_frame

-- React on a frame change.
-- This can be used to animate a widget.

-- (From EM_WIDGET)

theme_update

-- Update all display data according to new theme.

-- (From EM_WIDGET)

feature -- Basic operations

fire_clicked_event

-- File a clicked event.

feature -- Drawing

draw

-- Draw Current.

-- (From EM_COMPONENT)

draw_body

-- Draw widget body.

-- (From EM_WIDGET)

finish_drawing

-- Finish drawing Current.

-- (From EM_COMPONENT)

prepare_drawing

-- Prepare for drawing Current.

-- (From EM_COMPONENT)

redraw

-- Redraw Current.

-- (From EM_COMPONENT)

feature -- Events

clicked_event: EM_EVENT_TYPE [TUPLE []]

-- Clicked event

focus_lost_event: EM_EVENT_TYPE [TUPLE []]

-- Focus lost event

-- (From EM_KEYBOARD_SENSITIVE)

focus_received_event: EM_EVENT_TYPE [TUPLE []]

-- Focus received event

-- (From EM_KEYBOARD_SENSITIVE)

hide_event: EM_EVENT_TYPE [TUPLE []]

-- Component hidden event

-- (From EM_COMPONENT)

joystick_button_down_event: EM_EVENT_TYPE [TUPLE [EM_JOYSTICK_BUTTON_EVENT]]

-- Joystick button down event

-- (From EM_JOYSTICK_SENSITIVE)

key_down_event: EM_EVENT_TYPE [TUPLE [EM_KEYBOARD_EVENT]]

-- Key down event

-- (From EM_KEYBOARD_SENSITIVE)

key_up_event: EM_EVENT_TYPE [TUPLE [EM_KEYBOARD_EVENT]]

-- Key up event

-- (From EM_KEYBOARD_SENSITIVE)

mouse_button_down_event: EM_EVENT_TYPE [TUPLE[EM_MOUSEBUTTON_EVENT]]

-- Mouse button down event

-- (From EM_MOUSE_SENSITIVE)

mouse_button_up_event: EM_EVENT_TYPE [TUPLE[EM_MOUSEBUTTON_EVENT]]

-- Mouse button up event

-- (From EM_MOUSE_SENSITIVE)

mouse_clicked_event: EM_EVENT_TYPE [TUPLE[EM_MOUSEBUTTON_EVENT]]

-- Mouse clicked event

-- (From EM_MOUSE_SENSITIVE)

mouse_drag_start_event: EM_EVENT_TYPE [TUPLE[EM_MOUSE_EVENT]]

-- Mouse drag start event

-- (From EM_MOUSE_SENSITIVE)

mouse_drag_stop_event: EM_EVENT_TYPE [TUPLE[EM_MOUSE_EVENT]]

-- Mouse drag stop event

-- (From EM_MOUSE_SENSITIVE)

mouse_dragged_event: EM_EVENT_TYPE [TUPLE[EM_MOUSEMOTION_EVENT]]

-- Mouse dragged event

-- (From EM_MOUSE_SENSITIVE)

mouse_entered_event: EM_EVENT_TYPE [TUPLE []]

-- Mouse entered event

-- (From EM_MOUSE_SENSITIVE)

mouse_exited_event: EM_EVENT_TYPE [TUPLE []]

-- Mouse exited event

-- (From EM_MOUSE_SENSITIVE)

mouse_moved_event: EM_EVENT_TYPE [TUPLE[EM_MOUSEMOTION_EVENT]]

-- Mouse moved event

-- (From EM_MOUSE_SENSITIVE)

mouse_wheel_down_event: EM_EVENT_TYPE [TUPLE []]

-- Mouse wheel down event

-- (From EM_MOUSE_SENSITIVE)

mouse_wheel_up_event: EM_EVENT_TYPE [TUPLE []]

-- Mouse wheel up event

-- (From EM_MOUSE_SENSITIVE)

move_event: EM_EVENT_TYPE [TUPLE []]

-- Component moved event

-- (From EM_COMPONENT)

resize_event: EM_EVENT_TYPE [TUPLE []]

-- Component resized event

-- (From EM_COMPONENT)

show_event: EM_EVENT_TYPE [TUPLE []]

-- Component shown event

-- (From EM_COMPONENT)

feature {EM_COMPONENT_SCENE, EM_COMPONENT} -- Mouse management

mouse_button_down (event: EM_MOUSEBUTTON_EVENT)

-- Handle mouse button down event.

-- (From EM_COMPONENT)

mouse_button_up (event: EM_MOUSEBUTTON_EVENT)

-- Handle mouse button down event.
-- Set new keyboard focus if applicable.

-- (From EM_COMPONENT)

mouse_clicked (event: EM_MOUSEBUTTON_EVENT)

-- Handle mouse clicked event.

-- (From EM_COMPONENT)

mouse_drag_start (event: EM_MOUSE_EVENT)

-- Handle mouse drag start event.

-- (From EM_COMPONENT)

mouse_drag_stop (event: EM_MOUSE_EVENT)

-- Handle mouse-drag drop event.

-- (From EM_COMPONENT)

mouse_dragged (event: EM_MOUSEMOTION_EVENT)

-- Handle mouse dragging event.

-- (From EM_COMPONENT)

mouse_entered

-- Handle mouse entered event.

-- (From EM_COMPONENT)

mouse_exited

-- Handle mouse exited event.

-- (From EM_COMPONENT)

mouse_focus: EM_COMPONENT

-- Child with mouse focus

-- (From EM_WIDGET)

mouse_moved (event: EM_MOUSEMOTION_EVENT)

-- Handle mouse motion event.

-- (From EM_COMPONENT)

mouse_wheel_down

-- Handle mouse wheel down event.

-- (From EM_COMPONENT)

mouse_wheel_up

-- Handle mouse wheel up event.

-- (From EM_COMPONENT)

set_mouse_focus (mouse_x, mouse_y: INTEGER)

-- Set component at position mouse_x mouse_y to mouse_focus
-- or set mouse_focuse to Void if no component is at the given position.

-- (From EM_WIDGET)

feature {EM_WIDGET, EM_BACKGROUND, EM_BORDER} -- Implementation

child_changed (a_widget: EM_WIDGET)

-- Tell Current that nested widget a_widget has changed.

-- (From EM_WIDGET)

require
a_widget_is_child: has_widget (a_widget)
ensure
changed: is_changed
parent_widget: EM_WIDGET

-- Parent of this widget. The changed status will be forwarded to the parent.

-- (From EM_WIDGET)

set_parent (a_widget: EM_WIDGET)

-- Set parent_widget to a_widget.
-- If the parent is alredy set, this widget will be removed from the old parent!

-- (From EM_WIDGET)

ensure
parent_widget_set: parent_widget = a_widget
top_parent: EM_WIDGET

-- Topmost parent or Current if no parent is set

-- (From EM_WIDGET)

ensure
parent_of_parent: parent_widget /= Void implies Result = parent_widget.top_parent
current_if_no_parent: parent_widget = Void implies Result = Current
top_parent_not_void: Result /= Void

invariant

text_not_void: text /= Void
clicked_event_not_void: clicked_event /= Void

-- From EM_WIDGET
border_not_void: border /= Void

-- From EM_COMPONENT
make_component_called: is_make_component_called
resize_event_not_void: resize_event /= Void
move_event_not_void: move_event /= Void
hide_event_not_void: hide_event /= Void
show_event_not_void: show_event /= Void

key_down_event_not_void: key_down_event /= Void
key_up_event_not_void: key_up_event /= Void
focus_received_event_not_void: focus_received_event /= Void
focus_lost_event_not_void: focus_lost_event /= Void

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

mouse_button_down_event_not_void: mouse_button_down_event /= Void
mouse_button_up_event_not_void: mouse_button_up_event /= Void
mouse_clicked_event_not_void: mouse_clicked_event /= Void
mouse_moved_event_not_void: mouse_moved_event /= Void
mouse_dragged_event_not_void: mouse_dragged_event /= Void
mouse_drag_start_event_not_void: mouse_drag_start_event /= Void
mouse_drag_stop_event_not_void: mouse_drag_stop_event /= Void
mouse_wheel_up_event_not_void: mouse_wheel_up_event /= Void
mouse_wheel_down_event_not_void: mouse_wheel_down_event /= Void
mouse_entered_event_not_void: mouse_entered_event /= Void
mouse_exited_event_not_void: mouse_exited_event /= Void

joystick_axis_event_not_void: joystick_axis_event /= Void
joystick_ball_event_not_void: joystick_ball_event /= Void
joystick_button_down_event_not_void: joystick_button_down_event /= Void
joystick_button_up_event_not_void: joystick_button_up_event /= Void
joystick_hat_event_not_void: joystick_hat_event /= Void

end