indexing

	description: "[

		This interface represents an video decoder

	]"
	date: "$Date$"
	revision: "$Revision$"

deferred class

	EM_VIDEO_DECODER

inherit

	EM_DRAWABLE

	EM_SHARED_SUBSYSTEMS
		export {NONE} all end

feature {EM_VIDEO_DECODER_FACTORY} -- Load

	load_from_file (file: KI_BINARY_INPUT_FILE) is
			-- load video from file
		require
			not_loaded: not is_loaded
			file_exist: file /= Void and file.exists
			file_readable: file.is_open_read
			accept_file: accept_file (file)
			valid_file: is_valid_file (file)
		deferred
		ensure
			loaded: is_loaded
		end

feature -- Play

	play (loops: INTEGER) is
			-- play video
			-- Loops may be any valid number
			-- Special numbers are:
			--	-1: Plays forever
			--	 0: Plays this video zero times
		require
			loaded: is_loaded
			not_playing: not is_playing
			not_paused: not is_paused
			loops_valid: loops >= -1
		deferred
		ensure
			playing: is_playing
			not_paused: not is_paused
		end

feature -- Pause

	pause is
			-- pause playback
		require
			loaded: is_loaded
			playing: is_playing
		deferred
		ensure
			not_playing: not is_playing
			paused: is_paused
		end

	resume is
			-- resume playback
		require
			loaded: is_loaded
			paused: is_paused
		deferred
		ensure
			playing: is_playing
			not_paused: not is_paused
		end

feature -- Stop

	stop is
			-- stop playback
		require
			loaded: is_loaded
			not_stopped: is_playing or is_paused
		deferred
		ensure
			not_playing: not is_playing
			not_paused: not is_paused
		end

feature -- Status setting

	rewind is
			-- go to start
		require
			loaded: is_loaded
			not_stopped: is_playing or is_paused
		deferred
		ensure
			at_start: position <= 20
		end

	go_to_position (abs: INTEGER) is
			-- go to absolute position
		require
			loaded: is_loaded
			not_stopped: is_playing or is_paused
			valid_position: abs >= 0 and abs <= video_length
		deferred
		ensure
			position_set: position >= abs and position <= abs + 20
		end

	seek (interval: INTEGER) is
			-- seek interval time
		require
			loaded: is_loaded
			not_stopped: is_playing or is_paused
		deferred
		ensure
			seeked: (position >= (old position + interval) \\ video_length
								and (position <= (old position + interval + 20) \\ video_length or old position + interval + 20 >= video_length))
							or position <= 20 or position = video_length
		end

feature -- Event

	on_stop: EM_EVENT_CHANNEL [TUPLE] is
			-- event when playback stops
		deferred
		ensure
			exist: Result /= Void
		end

feature {EM_VIDEO_DECODER_FACTORY} -- Request

	is_valid_file (file: KI_BINARY_INPUT_FILE): BOOLEAN is
			-- is this file valid
		require
			file_exist: file /= Void and then file.exists
			file_open_read: file.is_open_read
			accepted: accept_file (file)
		deferred
		end

	accept_file (file: KI_BINARY_INPUT_FILE): BOOLEAN is
			-- can this file be handeld
		require
			file_exist: file /= Void and then file.exists
			file_open_read: file.is_open_read
		deferred
		end

feature -- Status report

	is_loaded: BOOLEAN

	is_paused: BOOLEAN

	is_playing: BOOLEAN

	has_audio: BOOLEAN

	has_video: BOOLEAN

	position: INTEGER is
			-- time played in ms
		deferred
		ensure
			in_range: Result >= 0 and Result <= video_length
		end

	video_length: INTEGER is
			-- video length in ms
		deferred
		ensure
			positive: Result >= 0
		end

	width: INTEGER

	height: INTEGER

	type: STRING is
			-- type of movie
		deferred
		ensure
			Result_set: Result /= Void and then not Result.is_empty
		end

	file_name: STRING is
			-- name of file
		deferred
		ensure
			Result_set: is_loaded implies Result /= Void
		end

invariant
	at_most_one_state: not (is_paused and is_playing)
	has_video_correct: has_video implies width > 0 and height > 0

end