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

em.timer

Class EM_TIMER


Direct ancestors

COMPARABLE, EM_TIME_SINGLETON

Creation

Features

Invariants

indexing

description

EM_TIMER is used by EM_TIME to hold a list of
callbacks.

date

$Date: 2005/10/23 10:31:22 $

revision

$Revision: 1.3 $

class

EM_TIMER

inherit

COMPARABLE
PART_COMPARABLE
EM_TIME_SINGLETON

create

make (an_integer: INTEGER; an_action: FUNCTION[ANY, TUPLE[INTEGER], INTEGER])

-- Create a EM_TIMER with callback an_action that is triggered evere an_integer milliseconds

require
positiv_interval: an_integer > 0
an_action_not_void: an_action /= void
ensure
interval = an_integercallback = an_actionnext_trigger_time = interval + time.ticks

feature -- Access

time: EM_TIME

-- Returns reference to the singleton

-- (From EM_TIME_SINGLETON)

ensure
time_not_void: Result /= Void

feature -- Comparison

infix "<=" (other: like Current): BOOLEAN

-- Is current object less than or equal to other?

-- (From PART_COMPARABLE)

require
other_exists: other /= Void
ensure then
definition: Result = ((Current < other) or is_equal (other))
infix ">" (other: like Current): BOOLEAN

-- Is current object greater than other?

-- (From PART_COMPARABLE)

require
other_exists: other /= Void
ensure then
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN

-- Is current object greater than or equal to other?

-- (From PART_COMPARABLE)

require
other_exists: other /= Void
ensure then
definition: Result = (other <= Current)
is_equal (other: like Current): BOOLEAN

-- Is other attached to an object of the same type
-- as current object and identical to it?

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then
trichotomy: Result = (not (Current < other) and not (other < Current))
max (other: like Current): like Current

-- The greater of current object and other

-- (From COMPARABLE)

require
other_exists: other /= Void
ensure
current_if_not_smaller: Current >= other implies Result = Current
other_if_smaller: Current < other implies Result = other
min (other: like Current): like Current

-- The smaller of current object and other

-- (From COMPARABLE)

require
other_exists: other /= Void
ensure
current_if_not_greater: Current <= other implies Result = Current
other_if_greater: Current > other implies Result = other
three_way_comparison (other: like Current): INTEGER

-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1

-- (From COMPARABLE)

require
other_exists: other /= Void
ensure
equal_zero: (Result = 0) = is_equal (other)
smaller_negative: (Result = -1) = (Current < other)
greater_positive: (Result = 1) = (Current > other)

feature {EM_TIME, EM_TIMER} -- status

callback: FUNCTION[ANY, TUPLE[INTEGER], INTEGER]

-- The function to be called at next_trigger_time

infix "<" (other: like Current): BOOLEAN

-- Is current EM_TIMER less than other?

-- (From PART_COMPARABLE)

require
other_exists: other /= Void
ensure then
asymmetric: Result implies not (other < Current)
interval: INTEGER

-- The interval in milliseconds between two calls of the callback

next_trigger_time: INTEGER

-- Next time in millisecond when the callback is will be called

set_interval (an_integer: INTEGER)

-- set interval to an_interval

require
an_integer > 0
ensure
interval = an_integer
set_next_trigger_time (an_integer: INTEGER)
require
an_integer > next_trigger_time
ensure
next_trigger_time = an_integer

invariant

-- From COMPARABLE
irreflexive_comparison: not (Current < Current)

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

end