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

em.video.figure

Class EM_POLYGON


Direct ancestors

EM_MULTI_POINTED_FIGURE, EM_CLOSED_FIGURE, DOUBLE_MATH

Creation

Features

Invariants

indexing

description

A polygon drawable in EiffelMedia

date

$Date: 2005/10/23 16:50:15 $

revision

$Revision: 1.9 $

class

EM_POLYGON

inherit

EM_MULTI_POINTED_FIGURE
EM_CLOSED_FIGURE

create

make_empty

-- Initialize with no points.

-- (From EM_MULTI_POINTED_FIGURE)

ensure
points_are_empty: is_empty
make_from_array (a_point_array: ARRAY [EM_VECTOR_2D])

-- Initialize with points in a_point_array.

-- (From DS_LINKED_LIST)

require
other_not_void: other /= Void
ensure
count_set: count = other.count
before: before
make_from_list (a_point_list: LIST [EM_VECTOR_2D])

-- Initialize with points in a_point_list

-- (From EM_MULTI_POINTED_FIGURE)

require
a_point_list_not_void: a_point_list /= Void
ensure
correct_position: before
filled: count = a_point_list.count
make_regular (n: INTEGER; first_point, first_edge: EM_VECTOR_2D)

-- Create a regular polygon with n points.
-- Starting with first_point and going into direction of first_edge (clockwise).

require
at_least_3_points: n >= 3
first_point_not_void: first_point /= Void
first_edge_not_void: first_edge /= Void
first_edge_not_zero: first_edge.length > 0
ensure
polygon_with_n_points_created: count = n
first_point_set: first.is_equal (first_point)

feature -- Initialization

default_create

-- Initialize Current as filled figure
-- in white colors with line width of 0.0.

-- (From ANY)

make_regular (n: INTEGER; first_point, first_edge: EM_VECTOR_2D)

-- Create a regular polygon with n points.
-- Starting with first_point and going into direction of first_edge (clockwise).

require
at_least_3_points: n >= 3
first_point_not_void: first_point /= Void
first_edge_not_void: first_edge /= Void
first_edge_not_zero: first_edge.length > 0
ensure
polygon_with_n_points_created: count = n
first_point_set: first.is_equal (first_point)

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_VECTOR_2D]

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

-- (From DS_SEARCHABLE)

first: EM_VECTOR_2D

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

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

-- (From DS_INDEXABLE)

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

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

-- (From DS_INDEXABLE)

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

-- Item at internal cursor position

-- (From DS_TRAVERSABLE)

require
not_off: not off
last: EM_VECTOR_2D

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

-- (From DS_BILINEAR)

require
not_empty: not is_empty
ensure
has_last: has (Result)
new_cursor: DS_LINKED_LIST_CURSOR [EM_VECTOR_2D]

-- 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_VECTOR_2D): 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
fill_color: EM_COLOR

-- The color with which the interrior of the figure is drawed,
-- if is_filled is True

-- (From EM_CLOSED_FIGURE)

has (v: EM_VECTOR_2D): 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
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_filled: BOOLEAN

-- Is Current drawed filled with fill_color?
-- (otherwise only the border will be drawed)

-- (From EM_CLOSED_FIGURE)

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)

line_color: EM_COLOR

-- Line color used to draw Current

-- (From EM_FIGURE)

line_width: DOUBLE

-- Line width used to draw Current

-- (From EM_FIGURE)

off: BOOLEAN

-- Is there no item at internal cursor position?

-- (From DS_TRAVERSABLE)

same_equality_tester (other: DS_SEARCHABLE [EM_VECTOR_2D]): BOOLEAN

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

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: EM_VECTOR_2D): 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
sorted (a_sorter: DS_SORTER [EM_VECTOR_2D]): 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_VECTOR_2D]): 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))
x: INTEGER

-- Horizontal position, distance in pixels from left

-- (From EM_DRAWABLE)

y: INTEGER

-- Vertical position, distance in pixels from top

-- (From EM_DRAWABLE)

feature -- Status setting

set_fill_color (a_color: EM_COLOR)

-- Set fill_color to a_color.

-- (From EM_CLOSED_FIGURE)

require
a_color_not_void: a_color /= Void
ensure
fill_color_assigned: fill_color = a_color
set_filled (a_bool: BOOLEAN)

-- Set is_filled to a_bool.

-- (From EM_CLOSED_FIGURE)

ensure
is_filled_set: is_filled = a_bool
set_line_color (a_color: EM_COLOR)

-- Set line_color to a_color.

-- (From EM_FIGURE)

require
a_color_not_void: a_color /= Void
ensure
line_color_assigned: line_color = a_color
set_line_width (a_width: DOUBLE)

-- Set line_width to a_width.

-- (From EM_FIGURE)

require
a_width_not_negative: a_width >= 0
ensure
line_width_set: line_width = a_width
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 (x_position: INTEGER; y_position: INTEGER)

-- Set x and y to x_position and y_position.
-- Moves all contained points accordingly.

-- (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
update_bounding_box

-- Recalculate bounding_box (x, y, width, height)
-- to surround all points.

-- (From EM_FIGURE)

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_VECTOR_2D)

-- 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_VECTOR_2D)

-- 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_VECTOR_2D]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_VECTOR_2D])

-- 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_VECTOR_2D])

-- 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_VECTOR_2D])

-- 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_VECTOR_2D]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_VECTOR_2D])

-- 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_VECTOR_2D]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_first (other: DS_LINEAR [EM_VECTOR_2D])

-- 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_VECTOR_2D])

-- 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_VECTOR_2D])

-- 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_VECTOR_2D]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_VECTOR_2D])

-- 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_VECTOR_2D]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_VECTOR_2D]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_VECTOR_2Di: 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_VECTOR_2D)

-- 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_VECTOR_2D)

-- 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_VECTOR_2D)

-- 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_VECTOR_2Da_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_VECTOR_2D)

-- 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_VECTOR_2Da_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_VECTOR_2Di: 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_VECTOR_2D)

-- 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_VECTOR_2D)

-- 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_VECTOR_2Da_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_VECTOR_2D)

-- 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_VECTOR_2Da_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_VECTOR_2Di: 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_VECTOR_2D)

-- 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_VECTOR_2Da_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_VECTOR_2D)

-- 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 in list.
-- Move all cursors off.
-- (Performance: O(count-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(count-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(2*a_cursor.index-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(count) if a_cursor.is_last, O(1) otherwise.)

-- (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(count).)

-- (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_cusor position.
-- Move any cursors at this position forth.
-- (Synonym of a_cursor.remove_left.)
-- (Performance: O(a_cursor.index).)

-- (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_VECTOR_2D]

-- 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 -- Basic operations

extend (point: EM_VECTOR_2D)

-- Add point to end of list.
-- Do not move cursors.
-- Also extend bounding_box to contain point.
-- (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
ensure then
bounding_box_extended: bounding_box.has (point)

feature -- Drawing

draw (surface: EM_SURFACE)

-- Draw Current onto 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 -- Mouse Events

has_crossing: BOOLEAN

-- do 2 lines of the polygon cross each other?

is_convex: BOOLEAN

-- is the polygon convex?

is_inside (a_point: EM_VECTOR_2D): BOOLEAN

-- Is a_point inside boundaries of Current.

is_on_border_line (a_point: EM_VECTOR_2D): BOOLEAN

-- Is a_point on boundary line of Current?

publish_mouse_event (a_mouse_event: EM_MOUSE_EVENT)

-- Publish mouse event when a_mouse_event occured on Current.
-- Only publish mouse event, if proportional_point lies on a point.

-- (From EM_DRAWABLE)

require
a_mouse_event_not_void: a_mouse_event /= 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(a_cursor.index).)

-- (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(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_VECTOR_2D

-- 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_VECTOR_2D)

-- 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.
-- (Performance: O(a_cursor.index).)

-- (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_VECTOR_2D)

-- 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_VECTOR_2D])

-- 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 -- Mouse events

events_initialized: BOOLEAN

-- Have events been initialized?

-- (From EM_DRAWABLE)

initialize_events

-- Event initialization.
-- Needs to be called before subscribing for events.

-- (From EM_DRAWABLE)

require
not_yet_initialized: not events_initialized
ensure
events_initialized: events_initialized
mouse_button_down_event_initialized: mouse_button_down_event /= Void
mouse_button_up_event_initialized: mouse_button_up_event /= Void
mouse_motion_event_initialized: mouse_motion_event /= Void
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 -- 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
height: INTEGER

-- Height of Current defining its bounding_box (x, y, width, height).

-- (From EM_DRAWABLE)

ensure
result_not_negative: Result >= 0
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
width: INTEGER

-- Width of Current defining its bounding_box (x, y, width, height).

-- (From EM_DRAWABLE)

ensure
result_not_negative: Result >= 0

feature {DS_LINKED_LIST, DS_LINKED_LIST_CURSOR} -- Implementation

first_cell: DS_LINKABLE [EM_VECTOR_2D]

-- First cell in list

-- (From DS_LINKED_LIST)

last_cell: like first_cell

-- Last cell in list

-- (From DS_LINKED_LIST)

invariant


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)

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

-- From EM_FIGURE
line_color_not_void: line_color /= Void
line_width_not_negative: line_width >= 0.0
points_not_void: points /= Void

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

fill_color_not_void: fill_color /= Void

end