deferred class interface ES_TIMEOUT_HANDLER
--
-- An object that the multiplexer will interrupt after a period of time.
--
feature(s) from ES_MULTIPLEXER_SINGLETON
-- The Multiplexer
multiplexer: ES_STANDALONE_MULTIPLEXER_POLL
-- The Multiplexer
ensure
not_void: Result /= Void
feature(s) from ES_TIMEOUT_HANDLER
-- Manage Timeouts
timeout_set: BOOLEAN
-- Is a timout set?
time_left: INTEGER
-- How much time left on clock?
require
timeout_set
ensure
non_negative: Result > 0
set_timeout (seconds: INTEGER)
-- Set for a timeout callback after aprox. seconds.
require
not_currently_set: not timeout_set;
non_negative: seconds >= 0
ensure
now_set: timeout_set;
time_left_proper: time_left <= seconds
stop_timeout
-- Stop the countdown.
require
currently_set: timeout_set
ensure
not_set: not timeout_set
end of deferred ES_TIMEOUT_HANDLER