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

em.video.container

Class EM_ZOOMABLE_WIDGET


Direct ancestors

EM_ZOOMABLE_CONTAINER

Creation

Features

Invariants

indexing

description

A widget that enables the user to zoom and scroll its content.

date

$Date: 2005/10/23 10:46:49 $

revision

$Revision: 1.4 $

class

EM_ZOOMABLE_WIDGET

inherit

EM_ZOOMABLE_CONTAINER

create

make (a_width, a_height: INTEGER)

-- Make empty container with size a_width and a_height.

-- (From EM_ZOOMABLE_CONTAINER)

ensure then
no_contained_drawables: is_empty
ensure then
no_contained_drawables: is_empty

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
equality_tester: KL_EQUALITY_TESTER [EM_DRAWABLE]

-- Equality tester;
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

first: EM_DRAWABLE

-- First item in list
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
not_empty: not is_empty
ensure
has_first: has (Result)
index: INTEGER

-- Index of current internal cursor position

-- (From DS_LIST)

ensure
valid_index: valid_index (Result)
infix "@" (i: INTEGER): EM_DRAWABLE

-- Item at index i
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
item (i: INTEGER): EM_DRAWABLE

-- Item at index i
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
item_for_iteration: EM_DRAWABLE

-- Item at internal cursor position

-- (From DS_TRAVERSABLE)

require
not_off: not off
last: EM_DRAWABLE

-- Last item in list
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
not_empty: not is_empty
ensure
has_last: has (Result)
new_cursor: DS_BILINKED_LIST_CURSOR [EM_DRAWABLE]

-- New external cursor for traversal

-- (From DS_TRAVERSABLE)

ensure
cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)

feature -- Measurement

count: INTEGER

-- Number of items in list
-- (Performance: O(1).)

-- (From DS_CONTAINER)

occurrences (v: EM_DRAWABLE): INTEGER

-- Number of times v appears in list
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
positive: Result >= 0
has: has (v) implies Result >= 1

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is list equal to other?
-- Do not take cursor positions nor
-- equality_tester into account.
-- (Performance: O(count).)

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

after: BOOLEAN

-- Is there no valid position to right of internal cursor?

-- (From DS_LINEAR)

before: BOOLEAN

-- Is there no valid position to left of internal cursor?

-- (From DS_BILINEAR)

equality_tester_settable (a_tester: like equality_tester): BOOLEAN

-- Can set_equality_tester be called with a_tester
-- as argument in current state of container?
-- (Default answer: True.)

-- (From DS_SEARCHABLE)

extendible (n: INTEGER): BOOLEAN

-- May list be extended with n items?

-- (From DS_EXTENDIBLE)

require
positive_n: n >= 0
ensure then
definition: Result = True
has (v: EM_DRAWABLE): BOOLEAN

-- Does list include v?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
not_empty: Result implies not is_empty
height: INTEGER

-- Height of Current container. Everything outside won't be drawed.

-- (From EM_DRAWABLE)

ensure
result_not_negative: Result >= 0
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_first: BOOLEAN

-- Is internal cursor on first item?

-- (From DS_LINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = first)
is_last: BOOLEAN

-- Is internal cursor on last item?

-- (From DS_BILINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = last)
is_size_fixed: BOOLEAN

-- Should Current not scale when drawed?
-- True means that the object will be drawed unscaled
-- but its position (reference_point) will still be transformed correctly
-- if drawed on a transformed scaled coordinate system
-- (This is handled accordingly by draw_object of EM_SURFACE)

-- (From EM_DRAWABLE)

max_zoom_factor: DOUBLE

-- Maximum zoom factor by which Current can be zoomed.

-- (From EM_ZOOMABLE_CONTAINER)

max_zoom_factor_bound: DOUBLE

-- Highest possible value for max_zoom_factor.

-- (From EM_ZOOMABLE_CONTAINER)

min_zoom_factor: DOUBLE

-- Minimum zoom factor by which Current can be zoomed.

-- (From EM_ZOOMABLE_CONTAINER)

min_zoom_factor_bound: DOUBLE

-- Lowest possible value for min_zoom_factor.

-- (From EM_ZOOMABLE_CONTAINER)

object_area: EM_ORTHOGONAL_RECTANGLE

-- Area inside which all contained drawable objects
-- should reside, scrolling is restricted to this area
-- (scrolling commands ensure to not to scroll center
-- of visible_area outside of object_area)

-- (From EM_ZOOMABLE_CONTAINER)

off: BOOLEAN

-- Is there no item at internal cursor position?

-- (From DS_TRAVERSABLE)

same_equality_tester (other: DS_SEARCHABLE [EM_DRAWABLE]): BOOLEAN

-- Does container use the same comparison
-- criterion as other?

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: EM_DRAWABLE): BOOLEAN

-- Are v and u considered equal?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

same_position (a_cursor: like new_cursor): BOOLEAN

-- Is internal cursor at same position as a_cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
size_factor: DOUBLE

-- Factor by which areas will be scaled (quadratic zoom_factor)

-- (From EM_ZOOMABLE_CONTAINER)

sorted (a_sorter: DS_SORTER [EM_DRAWABLE]): BOOLEAN

-- Is container sorted according to a_sorter's criterion?

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void
valid_cursor (a_cursor: DS_CURSOR [EM_DRAWABLE]): BOOLEAN

-- Is a_cursor a valid cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
valid_index (i: INTEGER): BOOLEAN

-- Is i a valid index value?

-- (From DS_LIST)

ensure
definition: Result = (0 <= i and i <= (count + 1))
visible_area: EM_ORTHOGONAL_RECTANGLE

-- Area defining coordinate system,
-- coordinates inside this area will be stretched
-- into area occupied by Current
-- (bounding_box)

-- (From EM_ZOOMABLE_CONTAINER)

width: INTEGER

-- Width of Current container. Everything outside won't be drawed.

-- (From EM_DRAWABLE)

ensure
result_not_negative: Result >= 0
x: INTEGER

-- Horizontal position, distance in pixels from left

-- (From EM_DRAWABLE)

y: INTEGER

-- Vertical position, distance in pixels from top

-- (From EM_DRAWABLE)

zoom_factor: DOUBLE

-- Factor by which lengths will be scaled.

-- (From EM_ZOOMABLE_CONTAINER)

zoom_factor_precision: DOUBLE

-- Precision of zoom_factor
-- (zoom factor's not differing more than this value are considered as equal).

-- (From EM_ZOOMABLE_CONTAINER)

feature -- Status setting

calculate_object_area

-- Calculate object_area from all contained objects
-- to tightly surround them.

-- (From EM_ZOOMABLE_CONTAINER)

set_max_zoom_factor (a_zoom_factor: DOUBLE)

-- Set max_zoom_factor to a_zoom_factor.
-- Adopt current zoom_factor to be in range, if necessary.

-- (From EM_ZOOMABLE_CONTAINER)

require
a_zoom_factor_is_valid_maximum: a_zoom_factor <= max_zoom_factor_bound
a_zoom_factor_above_minimum: a_zoom_factor >= min_zoom_factor
ensure
max_zoom_factor_set: max_zoom_factor = a_zoom_factor
set_min_zoom_factor (a_zoom_factor: DOUBLE)

-- Set min_zoom_factor to a_zoom_factor.
-- Adopt current zoom_factor to be in range, if necessary.

-- (From EM_ZOOMABLE_CONTAINER)

require
a_zoom_factor_is_valid_maximum: a_zoom_factor <= max_zoom_factor_bound
a_zoom_factor_above_minimum: a_zoom_factor >= min_zoom_factor
ensure
min_zoom_factor_set: min_zoom_factor = a_zoom_factor
set_min_zoom_factor_to_fit_object_area

-- Set min_zoom_factor such that it is not possible to zoom
-- farther than until object_area fits exactly into Current.

-- (From EM_ZOOMABLE_CONTAINER)

ensure
min_zoom_factor_set_to_fit_object_area: min_zoom_factor = (width / object_area.width).min (height / object_area.height)
set_object_area (an_area: EM_ORTHOGONAL_RECTANGLE)

-- Set object_area to an_area.

-- (From EM_ZOOMABLE_CONTAINER)

require
an_area_not_void: an_area /= Void
ensure
object_area_set: object_area = an_area
set_size (a_width, a_height: INTEGER)

-- Set size of Current to a_width and a_height.
-- Adopt visible_area accordingly.

-- (From EM_ZOOMABLE_CONTAINER)

require
a_width_positive: a_width > 0
a_height_positive: a_height > 0
ensure
width_set: width = a_width
height_set: height = a_height
set_size_fixed (a_boolean: BOOLEAN)

-- Set is_size_fixed to a_boolean.

-- (From EM_DRAWABLE)

ensure
size_fixed_set: is_size_fixed = a_boolean
set_x (x_position: INTEGER)

-- Set x to x_position.

-- (From EM_DRAWABLE)

ensure
x_set: x = x_position
set_x_y (an_x, a_y: INTEGER)

-- Set x to an_x and y to a_y.

-- (From EM_DRAWABLE)

ensure
x_set: x = an_x
y_set: y = a_y
set_y (y_position: INTEGER)

-- Set y to y_position.

-- (From EM_DRAWABLE)

ensure
y_set: y = y_position
set_zoom_factor (a_zoom_factor: DOUBLE)

-- Zoom Current such as zoom_factor is a_zoom_factor.

-- (From EM_ZOOMABLE_CONTAINER)

require
zoom_factor_above_minimum: a_zoom_factor >= min_zoom_factor
zoom_factor_below_maximum: a_zoom_factor <= max_zoom_factor
ensure
zoom_factor_set: is_zoom_factor_equal (a_zoom_factor)
set_zoom_factor_range (a_min_zoom_factor, a_max_zoom_factor: DOUBLE)

-- Set max_zoom_factor to a_max_zoom_factor and
-- min_zoom_factor to a_min_zoom_factor.
-- Adopt current zoom_factor to be in range, if necessary.

-- (From EM_ZOOMABLE_CONTAINER)

require
min_less_than_max: a_min_zoom_factor <= a_max_zoom_factor
a_min_zoom_factor_is_valid_minimum: a_min_zoom_factor >= min_zoom_factor_bound
a_max_zoom_factor_is_valid_maximum: a_max_zoom_factor <= max_zoom_factor_bound
ensure
min_zoom_factor_set: min_zoom_factor = a_min_zoom_factor
max_zoom_factor_set: max_zoom_factor = a_max_zoom_factor

feature -- Cursor movement

back

-- Move internal cursor to previous position.

-- (From DS_BILINEAR)

require
not_before: not before
finish

-- Move internal cursor to last position.

-- (From DS_BILINEAR)

ensure
empty_behavior: is_empty implies before
not_empty_behavior: not is_empty implies is_last
forth

-- Move internal cursor to next position.

-- (From DS_LINEAR)

require
not_after: not after
go_after

-- Move internal cursor to after position.

-- (From DS_LINEAR)

ensure
after: after
go_before

-- Move internal cursor to before position.

-- (From DS_BILINEAR)

ensure
before: before
go_i_th (i: INTEGER)

-- Move internal cursor to i-th position.

-- (From DS_LIST)

require
valid_index: valid_index (i)
ensure
moved: index = i
go_to (a_cursor: like new_cursor)

-- Move internal cursor to a_cursor's position.

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
ensure
same_position: same_position (a_cursor)
search_back (v: EM_DRAWABLE)

-- Move internal cursor to first position at or before current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.

-- (From DS_BILINEAR)

require
not_off: not off or before
search_forth (v: EM_DRAWABLE)

-- Move internal cursor to first position at or after current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
not_off: not off or after
start

-- Move internal cursor to first position.

-- (From DS_LINEAR)

ensure
empty_behavior: is_empty implies after
not_empty_behavior: not is_empty implies is_first

feature -- Element change

append (other: DS_LINEAR [EM_DRAWABLE]i: INTEGER)

-- Add items of other at i-th position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(i+other.count).)

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
append_first (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to beginning of list.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(other.count).)

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
append_last (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to end of list.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(other.count).)

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
append_left (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to left of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
not_before: not before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old index) = other.first)
append_left_cursor (other: DS_LINEAR [EM_DRAWABLE]a_cursor: like new_cursor)

-- Add items of other to left of a_cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Synonym of a_cursor.extend_left (other).)
-- (Performance: O(other.count).)

-- (From DS_LIST)

require
other_not_void: other /= Void
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old (a_cursor.index)) = other.first)
append_right (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to right of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
not_after: not after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (index + 1) = other.first)
append_right_cursor (other: DS_LINEAR [EM_DRAWABLE]a_cursor: like new_cursor)

-- Add items of other to right of a_cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Synonym of a_cursor.extend_right (other).)
-- (Performance: O(other.count).)

-- (From DS_LIST)

require
other_not_void: other /= Void
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
extend (v: EM_DRAWABLE)

-- Add v to end of list.
-- Do not move cursors.
-- (Performance: O(1).)

-- (From DS_EXTENDIBLE)

require
extendible: extendible (1)
ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
extend_first (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to beginning of list.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(other.count).)

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
extend_last (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to end of list.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(other.count).)

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
extend_left (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to left of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
not_before: not before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old index) = other.first)
extend_left_cursor (other: DS_LINEAR [EM_DRAWABLE]a_cursor: like new_cursor)

-- Add items of other to left of a_cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Synonym of a_cursor.extend_left (other).)
-- (Performance: O(other.count).)

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (old (a_cursor.index)) = other.first)
extend_right (other: DS_LINEAR [EM_DRAWABLE])

-- Add items of other to right of internal cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
not_after: not after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (index + 1) = other.first)
extend_right_cursor (other: DS_LINEAR [EM_DRAWABLE]a_cursor: like new_cursor)

-- Add items of other to right of a_cursor position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Synonym of a_cursor.extend_right (other).)
-- (Performance: O(other.count).)

-- (From DS_LIST)

require
other_not_void: other /= Void
extendible: extendible (other.count)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
new_count: count = old count + old other.count
same_order: (not other.is_empty) implies (item (a_cursor.index + 1) = other.first)
extend_with_list (other: DS_LINEAR [EM_DRAWABLE]i: INTEGER)

-- Add items of other at i-th position.
-- Keep items of other in the same order.
-- Do not move cursors.
-- (Performance: O(i+other.count).)

-- (From DS_INDEXABLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
force (v: EM_DRAWABLEi: INTEGER)

-- Add v at i-th position.
-- Do not move cursors.
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
force_first (v: EM_DRAWABLE)

-- Add v to beginning of list.
-- Do not move cursors.
-- (Performance: O(1).)

-- (From DS_INDEXABLE)

ensure
one_more: count = old count + 1
inserted: first = v
force_last (v: EM_DRAWABLE)

-- Add v to end of list.
-- Do not move cursors.
-- (Performance: O(1).)

-- (From DS_EXTENDIBLE)

ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
force_left (v: EM_DRAWABLE)

-- Add v to left of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
not_before: not before
ensure
one_more: count = old count + 1
force_left_cursor (v: EM_DRAWABLEa_cursor: like new_cursor)

-- Add v to left of a_cursor position.
-- Do not move cursors.
-- (Synonym of a_cursor.put_left (v).)
-- (Performance: O(1).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
one_more: count = old count + 1
force_right (v: EM_DRAWABLE)

-- Add v to right of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
not_after: not after
ensure
one_more: count = old count + 1
force_right_cursor (v: EM_DRAWABLEa_cursor: like new_cursor)

-- Add v to right of a_cursor position.
-- Do not move cursors.
-- (Synonym of a_cursor.put_right (v).)
-- (Performance: O(1).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
one_more: count = old count + 1
put (v: EM_DRAWABLEi: INTEGER)

-- Add v at i-th position.
-- Do not move cursors.
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
extendible: extendible (1)
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
put_first (v: EM_DRAWABLE)

-- Add v to beginning of list.
-- Do not move cursors.
-- (Performance: O(1).)

-- (From DS_INDEXABLE)

require
extendible: extendible (1)
ensure
one_more: count = old count + 1
inserted: first = v
put_left (v: EM_DRAWABLE)

-- Add v to left of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
extendible: extendible (1)
not_before: not before
ensure
one_more: count = old count + 1
put_left_cursor (v: EM_DRAWABLEa_cursor: like new_cursor)

-- Add v to left of a_cursor position.
-- Do not move cursors.
-- (Synonym of a_cursor.put_left (v).)
-- (Performance: O(1).)

-- (From DS_LIST)

require
extendible: extendible (1)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
ensure
one_more: count = old count + 1
put_right (v: EM_DRAWABLE)

-- Add v to right of internal cursor position.
-- Do not move cursors.

-- (From DS_LIST)

require
extendible: extendible (1)
not_after: not after
ensure
one_more: count = old count + 1
put_right_cursor (v: EM_DRAWABLEa_cursor: like new_cursor)

-- Add v to right of a_cursor position.
-- Do not move cursors.
-- (Synonym of a_cursor.put_right (v).)
-- (Performance: O(1).)

-- (From DS_LIST)

require
extendible: extendible (1)
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
ensure
one_more: count = old count + 1
replace (v: EM_DRAWABLEi: INTEGER)

-- Replace item at index i by v.
-- Do not move cursors.
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
ensure
same_count: count = old count
replaced: item (i) = v
replace_at (v: EM_DRAWABLE)

-- Replace item at internal cursor position by v.
-- Do not move cursors.

-- (From DS_LIST)

require
not_off: not off
ensure
same_count: count = old count
replaced: item_for_iteration = v
replace_at_cursor (v: EM_DRAWABLEa_cursor: like new_cursor)

-- Replace item at a_cursor position by v.
-- Do not move cursors.
-- (Synonym of a_cursor.replace (v).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_off: not a_cursor.off
ensure
same_count: count = old count
replaced: a_cursor.item = v
swap (i, j: INTEGER)

-- Exchange items at indexes i and j.
-- Do not move cursors.
-- (Performance: O(max(i,j)).)

-- (From DS_INDEXABLE)

require
valid_i: 1 <= i and i <= count
valid_j: 1 <= j and j <= count
ensure
same_count: count = old count
new_i: item (i) = old item (j)
new_j: item (j) = old item (i)

feature -- Removal

delete (v: EM_DRAWABLE)

-- Remove all occurrences of v.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move all cursors off.
-- (Performance: O(count).)

-- (From DS_LIST)

ensure
deleted: not has (v)
new_count: count = old (count - occurrences (v))
keep_first (n: INTEGER)

-- Keep n first items in list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
keep_last (n: INTEGER)

-- Keep n last items of list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
prune (n: INTEGER; i: INTEGER)

-- Remove n items at and after i-th position.
-- Move all cursors off.
-- (Performance: O(i+n).)

-- (From DS_INDEXABLE)

require
valid_index: 1 <= i and i <= count
valid_n: 0 <= n and n <= (count - i + 1)
ensure
new_count: count = old count - n
prune_first (n: INTEGER)

-- Remove n first items from list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_last (n: INTEGER)

-- Remove n last items from list.
-- Move all cursors off.
-- (Performance: O(n).)

-- (From DS_INDEXABLE)

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_left (n: INTEGER)

-- Remove n items to left of internal cursor position.
-- Move all cursors off.

-- (From DS_LIST)

require
valid_n: 0 <= n and n < index
ensure
new_count: count = old count - n
prune_left_cursor (n: INTEGER; a_cursor: like new_cursor)

-- Remove n items to left of a_cursor position.
-- Move all cursors off.
-- (Synonym of a_cursor.prune_left (n).)
-- (Performance: O(n).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
valid_n: 0 <= n and n < a_cursor.index
ensure
new_count: count = old count - n
prune_right (n: INTEGER)

-- Remove n items to right of internal cursor position.
-- Move all cursors off.

-- (From DS_LIST)

require
valid_n: 0 <= n and n <= (count - index)
ensure
new_count: count = old count - n
prune_right_cursor (n: INTEGER; a_cursor: like new_cursor)

-- Remove n items to right of a_cursor position.
-- Move all cursors off.
-- (Synonym of a_cursor.prune_right (n).)
-- (Performance: O(n).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
valid_n: 0 <= n and n <= (count - a_cursor.index)
ensure
new_count: count = old count - n
remove (i: INTEGER)

-- Remove item at i-th position.
-- Move any cursors at this position forth.
-- (Performance: O(i).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
valid_index: 1 <= i and i <= count
ensure
one_less: count = old count - 1
remove_at

-- Remove item at internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_off: not off
ensure
one_less: count = old count - 1
remove_at_cursor (a_cursor: like new_cursor)

-- Remove item at a_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove.)
-- (Performance: O(1).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_off: not a_cursor.off
ensure
one_less: count = old count - 1
remove_first

-- Remove item at beginning of list.
-- Move any cursors at this position forth.
-- (Performance: O(1).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_last

-- Remove item at end of list.
-- Move any cursors at this position forth.
-- (Performance: O(1).)

-- (From DS_INDEXABLE)

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_left

-- Remove item to left of internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_empty: not is_empty
not_before: not before
not_first: not is_first
ensure
one_less: count = old count - 1
remove_left_cursor (a_cursor: like new_cursor)

-- Remove item to left of a_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_left.)
-- (Performance: O(1).)

-- (From DS_LIST)

require
not_empty: not is_empty
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_before: not a_cursor.before
not_first: not a_cursor.is_first
ensure
one_less: count = old count - 1
remove_right

-- Remove item to right of internal cursor position.
-- Move any cursors at this position forth.

-- (From DS_LIST)

require
not_empty: not is_empty
not_after: not after
not_last: not is_last
ensure
one_less: count = old count - 1
remove_right_cursor (a_cursor: like new_cursor)

-- Remove item to right of a_cursor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_right.)
-- (Performance: O(1).)

-- (From DS_LIST)

require
not_empty: not is_empty
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
not_after: not a_cursor.after
not_last: not a_cursor.is_last
ensure
one_less: count = old count - 1
wipe_out

-- Remove all items from list.
-- Move all cursors off.
-- (Performance: O(1).)

-- (From DS_CONTAINER)

ensure
wiped_out: is_empty

feature -- Duplication

cloned_object: like Current

-- Clone of current object

-- (From KL_CLONABLE)

ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)
copy (other: like Current)

-- Copy other to current list.
-- Move all cursors off (unless other = Current).
-- (Performance: O(other.count).)

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)
to_array: ARRAY [EM_DRAWABLE]

-- Array containing the same items as current
-- container in the same order

-- (From DS_LINEAR)

ensure
to_array_not_void: Result /= Void
same_count: Result.count = count

feature -- Drawing

draw (a_surface: EM_SURFACE)

-- Draw Current to a_surface

-- (From EM_DRAWABLE)

require
a_surface_not_void: a_surface /= Void
draw_part (a_rect: EM_RECT; a_surface: EM_SURFACE)

-- Draw rectangular part of Current defined by a_rect to a_surface.
-- (Subclasses could redefine this feature for providing an implementation
-- with better performance, otherwise its just done per default by
-- transforming and clipping coordinates on a_surface before calling draw).

-- (From EM_DRAWABLE)

require
a_surface_not_void: a_surface /= Void
a_rect_not_void: a_rect /= Void

feature {DS_CURSOR} -- Cursor implementation

add_traversing_cursor (a_cursor: like new_cursor)

-- Add a_cursor to the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
cursor_after (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to right of a_cursor?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_back (a_cursor: like new_cursor)

-- Move a_cursor to previous position.
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_before: not cursor_before (a_cursor)
cursor_before (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to left of a_cursor?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_finish (a_cursor: like new_cursor)

-- Move a_cursor to last position.
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_before (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_last (a_cursor)
cursor_forth (a_cursor: like new_cursor)

-- Move a_cursor to next position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_after: not cursor_after (a_cursor)
cursor_go_after (a_cursor: like new_cursor)

-- Move a_cursor to after position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_after: cursor_after (a_cursor)
cursor_go_before (a_cursor: like new_cursor)

-- Move a_cursor to before position.
-- (Performance: O(1).)

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_before: cursor_before (a_cursor)
cursor_go_i_th (a_cursor: like new_cursor; i: INTEGER)

-- Move a_cursor to i-th position.
-- (Performance: O(min(i,count-i)).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
valid_index: valid_index (i)
ensure
moved: cursor_index (a_cursor) = i
cursor_go_to (a_cursor, other: like new_cursor)

-- Move a_cursor to other's position.
-- (Performance: O(1).)

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
other_valid: valid_cursor (other)
ensure
same_position: cursor_same_position (a_cursor, other)
cursor_index (a_cursor: like new_cursor): INTEGER

-- Index of a_cursor's current position
-- (Performance: O(count).)

-- (From DS_LIST)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
valid_index: valid_index (Result)
cursor_is_first (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on first item?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = first)
cursor_is_last (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on last item?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = last)
cursor_item (a_cursor: like new_cursor): EM_DRAWABLE

-- Item at a_cursor position
-- (Performance: O(1).)

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor)
cursor_off (a_cursor: like new_cursor): BOOLEAN

-- Is there no item at a_cursor position?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_same_position (a_cursor, other: like new_cursor): BOOLEAN

-- Is a_cursor at same position as other?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
cursor_search_back (a_cursor: like new_cursorv: EM_DRAWABLE)

-- Move a_cursor to first position at or before its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_before (a_cursor)
cursor_search_forth (a_cursor: like new_cursorv: EM_DRAWABLE)

-- Move a_cursor to first position at or after its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_after (a_cursor)
cursor_start (a_cursor: like new_cursor)

-- Move a_cursor to first position.
-- (Performance: O(1).)

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_after (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_first (a_cursor)
remove_traversing_cursor (a_cursor: like new_cursor)

-- Remove a_cursor from the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void

feature -- Sort

sort (a_sorter: DS_SORTER [EM_DRAWABLE])

-- Sort container using a_sorter's algorithm.

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void
ensure
sorted: sorted (a_sorter)

feature -- Setting

set_equality_tester (a_tester: like equality_tester)

-- Set equality_tester to a_tester.
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

require
equality_tester_settable: equality_tester_settable (a_tester)
ensure
equality_tester_set: equality_tester = a_tester

feature -- Commands

center_on (a_position: EM_VECTOR_2D)

-- Scroll to have a_position in the center of Current.

-- (From EM_ZOOMABLE_CONTAINER)

require
a_position_not_void: a_position /= Void
scroll (a_direction: EM_VECTOR_2D)

-- Scroll Current by a_direction
-- in object coordinates.

-- (From EM_ZOOMABLE_CONTAINER)

require
a_direction_not_void: a_direction /= Void
scroll_and_zoom_to_rectangle (an_area: EM_ORTHOGONAL_RECTANGLE)

-- Zoom and scroll to fit an_area into visible_area (centered)

-- (From EM_ZOOMABLE_CONTAINER)

require
an_area_not_void: an_area /= Void
scroll_proportional (a_direction: EM_VECTOR_2D)

-- Scroll Current by a_direction
-- in transformed coordinates

-- (From EM_ZOOMABLE_CONTAINER)

require
a_direction_not_void: a_direction /= Void
zoom (a_zoom_factor: DOUBLE)

-- Zoom Current by a_zoom_factor.

-- (From EM_ZOOMABLE_CONTAINER)

require
a_zoom_factor_is_positive: a_zoom_factor > 0
ensure
not_zoomed_over_zoom_max: zoom_factor <= max_zoom_factor + zoom_factor_precision
not_zoomed_over_zoom_min: zoom_factor >= min_zoom_factor - zoom_factor_precision

feature -- Mouse Events

mouse_button_down_on_item_event: EM_EVENT_TYPE [TUPLE [EM_DRAWABLE]]

-- Mouse button down on item event,
-- gets published when the mouse button event
-- is caught by an item inside Current,
-- item is passed as first argument to subscribers,
-- an EM_MOUSEBUTTON_EVENT is passed
-- as optional second argument

-- (From EM_DRAWABLE_CONTAINER)

mouse_button_up_on_item_event: EM_EVENT_TYPE [TUPLE [EM_DRAWABLE]]

-- Mouse button up on item event,
-- gets published when the mouse button event
-- is caught by an item inside Current,
-- item is passed as first argument to subscribers,
-- an EM_MOUSEBUTTON_EVENT is passed
-- as optional second argument

-- (From EM_DRAWABLE_CONTAINER)

mouse_motion_on_item_event: EM_EVENT_TYPE [TUPLE [EM_DRAWABLE]]

-- Mouse motion on item event,
-- gets published when the mouse motion event
-- is caught by an item inside Current,
-- item is passed as first argument to subscribers,
-- an EM_MOUSEBUTTON_EVENT is passed
-- as optional second argument

-- (From EM_DRAWABLE_CONTAINER)

publish_mouse_event (a_mouse_event: EM_MOUSE_EVENT)

-- Publish mouse event to children
-- when a_mouse_event occured on Current
-- (pass object coordinates to children).

-- (From EM_DRAWABLE)

require
a_mouse_event_not_void: a_mouse_event /= Void

feature -- Local Coordinate Transformation

object_point (a_x, a_y: DOUBLE): EM_VECTOR_2D

-- Point coordinate in object space that corresponds to position a_x and a_y on Current.

-- (From EM_ZOOMABLE_CONTAINER)

ensure
result_created: Result /= Void
transformed_object_point (a_point: EM_VECTOR_2D): EM_VECTOR_2D

-- Coordinates where a_point in object space is transformed to by Current (zoomed and/or scrolled).

-- (From EM_ZOOMABLE_CONTAINER)

require
a_point_not_void: a_point /= Void
ensure
result_created: Result /= Void

feature -- Zoom and Scroll Events

visible_area_changed_event: EM_EVENT_TYPE [TUPLE []]

-- Event when visible area has been changed (either zoomed or scrolled)

-- (From EM_ZOOMABLE_CONTAINER)

feature -- Queries

bounding_box: EM_ORTHOGONAL_RECTANGLE

-- Orthogonal rectangle surrounding Current; (i.e. usefull
-- for visibility testing if it intersects with
-- coordinate_area of EM_SURFACE) TODO: We create a new
-- one on each call. Maybe there is a more efficient way to
-- do that?

-- (From EM_DRAWABLE)

ensure
result_not_void: Result /= Void
is_zoom_factor_equal (a_zoom_factor: DOUBLE): BOOLEAN

-- Check if zoom_factor is considered equal to a_zoom_factor.
-- Zoom factors are considered as equal, if they don't differ by more than zoom_factor_precision.

-- (From EM_ZOOMABLE_CONTAINER)

reference_point: EM_VECTOR_2D

-- Reference point of Current relative to which it should be positioned.
-- (i.e. important when drawn on a scaled coordinate system and is_size_fixed is True)

-- (From EM_DRAWABLE)

ensure
result_not_void: Result /= Void

feature -- Mouse events

events_initialized: BOOLEAN

-- Have events been initialized?

-- (From EM_DRAWABLE)

mouse_button_down_event: EM_EVENT_TYPE [TUPLE [EM_MOUSE_EVENT]]

-- Mouse button down event,
-- gets published when the mouse button is pressed over Current,
-- an EM_MOUSEBUTTON_EVENT is passed as argument

-- (From EM_DRAWABLE)

mouse_button_up_event: EM_EVENT_TYPE [TUPLE [EM_MOUSE_EVENT]]

-- Mouse button up event,
-- gets published when the mouse button is released over Current,
-- an EM_MOUSEBUTTON_EVENT is passed as argument

-- (From EM_DRAWABLE)

mouse_motion_event: EM_EVENT_TYPE [TUPLE [EM_MOUSE_EVENT]]

-- Mouse button up event,
-- gets published when the mouse button is released over Current,
-- an EM_MOUSEMOTION_EVENT is passed as argument

-- (From EM_DRAWABLE)

feature {DS_LINKED_LIST, DS_LINKED_LIST_CURSOR} -- Implementation

first_cell: DS_BILINKABLE [EM_DRAWABLE]

-- First cell in list

-- (From DS_LINKED_LIST)

last_cell: like first_cell

-- Last cell in list

-- (From DS_LINKED_LIST)

invariant

min_zoom_factor_above_minimum_bound: min_zoom_factor >= min_zoom_factor_bound
max_zoom_factor_below_maximum_bound: max_zoom_factor <= max_zoom_factor_bound
min_zoom_factor_below_maximum_zoom_factor: min_zoom_factor <= max_zoom_factor
zoom_factor_above_minimum: zoom_factor >= min_zoom_factor - zoom_factor_precision
zoom_factor_below_maximum: zoom_factor <= max_zoom_factor + zoom_factor_precision

-- From EM_DRAWABLE
mouse_button_down_event_initialized: events_initialized implies mouse_button_down_event /= Void
mouse_button_up_event_initialized: events_initialized implies mouse_button_up_event /= Void
mouse_motion_event_initialized: events_initialized implies mouse_motion_event /= Void

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

first_constraint: first_cell /= Void implies first_cell.left = Void

first_cell: is_empty = (first_cell = Void)
last_cell: is_empty = (last_cell = Void)
last_constraint: last_cell /= Void implies last_cell.right = Void

-- From DS_BILINEAR
not_both: initialized implies (not (after and before))
before_constraint: initialized implies (before implies off)

-- From DS_LINEAR
after_constraint: initialized implies (after implies off)

empty_constraint: initialized implies (is_empty implies off)
internal_cursor_not_void: initialized implies (internal_cursor /= Void)
valid_internal_cursor: initialized implies valid_cursor (internal_cursor)

-- From DS_CONTAINER
positive_count: count >= 0
empty_definition: is_empty = (count = 0)

end