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

em.widget.widgets

Class EM_TEXTLIST


Direct ancestors

EM_LIST

Creation

Features

Invariants

indexing

description

A widget which displays a list of elements.

The elements are displayd as strings and the conversion agent
can be set using set_to_string_agent. By default the feature
out from ANY will be used.

See EM_LIST

date

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

revision

$Revision: 1.9 $

class

EM_TEXTLIST [G->ANY]

inherit

EM_LIST

create

make_empty

-- Initialise empty list.

make_from_list (a_list: DS_LINEAR [G])

-- Initialise list with elements from a_list.

feature -- Access

background: EM_BACKGROUND

-- Background of widget

-- (From EM_WIDGET)

border: EM_BORDER

-- Border of widget

-- (From EM_WIDGET)

delegate: EM_LIST_DELEGATE

-- Delegate which draws widget

-- (From EM_WIDGET)

elements: DS_LINEAR [G]

-- Linear representation of elements

-- (From EM_LIST)

font: EM_FONT

-- Font of widget

-- (From EM_WIDGET)

foreground_color: EM_COLOR

-- Foreground color of widget

-- (From EM_WIDGET)

screen_x: INTEGER

-- X position of Current on screen

-- (From EM_WIDGET)

screen_y: INTEGER

-- Y position of Current on screen

-- (From EM_WIDGET)

selected_element: G

-- Currently selected element

-- (From EM_LIST)

selected_index: INTEGER

-- Index of selected element

-- (From EM_LIST)

selection_background_color: EM_COLOR

-- Background on selected element

selection_foreground_color: EM_COLOR

-- Foreground on selected element

surface: EM_SURFACE

-- Surface to draw on

-- (From EM_2D_COMPONENT)

to_string_agent: FUNCTION [ANY, TUPLE [G], STRING]

-- Agent to convert elements to a string.

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

count: INTEGER

-- Number of elements in list

-- (From EM_LIST)

ensure
count_not_negative: count >= 0
consistent: Result = elements.count
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 (an_element: G): BOOLEAN

-- Is an_element in the list?

-- (From EM_LIST)

require
an_element_not_void: an_element /= Void
ensure
consistent: Result implies elements.has (an_element)
has_selected_element: BOOLEAN

-- Is any element selected?

-- (From EM_LIST)

ensure
consistent: Result implies selected_element /= Void
has_void_element: BOOLEAN

-- Is a void element present (at index 0)?

-- (From EM_LIST)

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_sensitive: BOOLEAN

-- Does Current handle mouse events?

-- (From EM_INPUT_SENSITIVE)

is_visible: BOOLEAN

-- Is Current visible?

-- (From EM_COMPONENT)

feature -- Status setting

disable

-- Disable widget.

-- (From EM_COMPONENT)

ensure
not_enabled: not is_enabled
ensure then
is_changed: is_changed
enable

-- Enable widget.

-- (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_sensitive (sensitive: BOOLEAN)

-- Set mouse sensitivity status.

-- (From EM_INPUT_SENSITIVE)

ensure
mouse_sensitivity_set: is_mouse_sensitive = sensitive
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
extend (a_list: DS_LINEAR [G])

-- Extend elements by a_list.

-- (From EM_LIST)

require
a_list_not_void: a_list /= Void
ensure
added: True
changed: is_changed
insert_void_element

-- Insert a void element at the beginning of the list (allows to deselect).
-- This element will not count as a normal element

-- (From EM_LIST)

ensure
has_void_element: has_void_element
count_not_changed: count = old count
changed: is_changed
put (an_element: G)

-- Extend elements by an_element.

-- (From EM_LIST)

require
an_element_not_void: an_element /= Void
ensure
added: has (an_element)
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_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_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_selected_element (an_element: G)

-- Set selected_element to an_element.

-- (From EM_LIST)

require
an_element_not_void: an_element /= Void
an_element_present: has (an_element)
ensure
selected_element_set: selected_element = an_element
changed: is_changed
set_selected_index (an_index: INTEGER)

-- Set selected_element to element at an_index.

-- (From EM_LIST)

require
an_index_valid: 1 <= an_index and an_index <= count
ensure
selected_index_set: selected_index = an_index
changed: is_changed
set_selection_background_color (a_color: like selection_background_color)

-- set the background color of the selected element to a_color.

require
a_color_not_void: a_color /= Void
ensure
selection_background_color_set: selection_background_color = a_color
changed: is_changed
set_selection_foreground_color (a_color: like selection_foreground_color)

-- set the foreground color of the selected element to a_color.

require
a_color_not_void: a_color /= Void
ensure
selection_foreground_color_set: selection_foreground_color = a_color
changed: is_changed
set_to_string_agent (an_agent: like to_string_agent)

-- Set to_string_agent to an_agent.

require
an_agent_not_void: an_agent /= Void
ensure
to_string_agent_set: to_string_agent = an_agent
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
sort (a_sorter: DS_SORTER [G])

-- Sort elements according to a_sorter.

-- (From EM_LIST)

ensure
sorted: a_sorter.sorted (elements_impl)
changed: is_changed
unselect

-- Clear selection

-- (From EM_LIST)

ensure
nothing_selected: not has_selected_element
changed: is_changed

feature -- Removal

remove (an_element: G)

-- Remove an_element from the list.

-- (From EM_LIST)

require
an_element_not_void: an_element /= Void
ensure
an_element_removed: not has (an_element)
changed: is_changed
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
wipe_out

-- Wipe out 'elements'.

-- (From EM_LIST)

ensure
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 -- 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

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)

selection_changed_event: EM_EVENT_TYPE [TUPLE [G]]

-- Selection change event

-- (From EM_LIST)

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
elements_impl: DS_LIST [G]

-- List of elements

-- (From EM_LIST)

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

-- From EM_LIST
element_selected: has_selected_element implies selected_element /= Void
index_selected: has_selected_element implies (1 <= selected_index and selected_index <= count)
selection_change_event_not_void: selection_changed_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