indexing
	description: "Repeatedly executes a sequence of `actions' at a regular `interval'."
	status: "See notice at end of class"
	keywords: "timout, delay, timer, background"
	date: "$Date$"
	revision: "$Revision$"

class interface
	EV_TIMEOUT

create 

	frozen default_create
			-- Standard creation procedure.
			-- (from EV_ANY)
		ensure then -- from EV_ANY
			is_coupled: implementation /= void
			is_initialized: is_initialized
			default_create_called_set: default_create_called
			is_in_default_state: is_in_default_state

	make_with_interval (an_interval: INTEGER)
			-- Create with an_interval in milliseconds.
		require
			an_interval_not_negative: an_interval >= 0

feature -- Access

	actions: EV_NOTIFY_ACTION_SEQUENCE
			-- Actions to be performed at a regular interval.
			-- Only called when interval is greater than 0.

	data: ANY
			-- Arbitrary user data may be stored here.
			-- (from EV_ANY)

	interval: INTEGER
			-- Time between calls to actions in milliseconds.
			-- If 0, then actions are disabled.
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result = implementation.interval

	set_interval (an_interval: INTEGER)
			-- Assign an_interval in milliseconds to interval.
			-- If an_interval is 0, actions are disabled.
		require
			not_destroyed: not is_destroyed
			an_interval_not_negative: an_interval >= 0
		ensure
			interval_assigned: interval = an_interval
			count_not_changed: count = old count
	
feature -- Status report

	count: INTEGER
			-- Number of times actions have been called since last
			-- call to reset_count.
		require
			not_destroyed: not is_destroyed
		ensure
			bridge_ok: Result = implementation.count
	
feature -- Status setting

	reset_count
			-- Set count to 0.
		require
			not_destroyed: not is_destroyed
		ensure
			count_is_zero: count = 0
	
feature -- Element change

	set_data (some_data: like data)
			-- Assign some_data to data.
			-- (from EV_ANY)
		require -- from EV_ANY
			not_destroyed: not is_destroyed
		ensure -- from EV_ANY
			data_assigned: data = some_data
	
feature -- Duplication

	copy (other: like Current)
			-- Update current object using fields of object attached
			-- to other, so as to yield equal objects.
			-- (from EV_ANY)
		require -- from ANY
			other_not_void: other /= void
			type_identity: same_type (other)
		ensure -- from ANY
			is_equal: is_equal (other)
	
feature -- Command

	destroy
			-- Destroy underlying native toolkit object.
			-- Render Current unusable.
			-- (from EV_ANY)
		ensure -- from EV_ANY
			is_destroyed: is_destroyed
	
feature -- Status Report

	is_destroyed: BOOLEAN
			-- Is Current no longer usable?
			-- (from EV_ANY)
		ensure -- from EV_ANY
			bridge_ok: Result = implementation.is_destroyed
	
invariant

	interval_not_negative: interval >= 0
	count_not_negative: count >= 0
	actions_not_void: actions /= void
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from EV_ANY
	is_initialized: is_initialized
	is_coupled: implementation /= void and then implementation.interface = Current
	default_create_called: default_create_called

end -- class EV_TIMEOUT