indexing
	description: "Facilities for direct drawing on the screen."
	status: "See notice at end of class"
	keywords: "screen, root, window, visual, top"
	date: "$Date$"
	revision: "$Revision$"

class interface
	EV_SCREEN

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

feature -- Access

	background_color: EV_COLOR
			-- Color displayed behind foreground features.
			-- (from EV_COLORIZABLE)
		require -- from EV_COLORIZABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_COLORIZABLE
			bridge_ok: Result.is_equal (implementation.background_color)

	clip_area: EV_RECTANGLE
			-- Rectangular area to apply clipping on.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			bridge_ok: (Result = void) = (implementation.clip_area = void)

	dashed_line_style: BOOLEAN
			-- Are lines drawn dashed?
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			bridge_ok: Result = implementation.dashed_line_style

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

	drawing_mode: INTEGER
			-- Logical operation on pixels when drawing.
			-- Default: drawing_mode_copy.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			bridge_ok: Result = implementation.drawing_mode

	font: EV_FONT
			-- Typeface appearance for Current.
			-- (from EV_FONTABLE)
		require -- from EV_FONTABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_FONTABLE
			not_void: Result /= void
			bridge_ok: Result.is_equal (implementation.font)

	foreground_color: EV_COLOR
			-- Color of foreground features like text.
			-- (from EV_COLORIZABLE)
		require -- from EV_COLORIZABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_COLORIZABLE
			bridge_ok: Result.is_equal (implementation.foreground_color)

	line_width: INTEGER
			-- Line thickness. Default: 1.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			bridge_ok: Result = implementation.line_width

	tile: EV_PIXMAP
			-- Pixmap that is used to draw filled primitives with
			-- instead of foreground_color.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			bridge_ok: (Result = void) = (implementation.tile = void)
	
feature -- Measurement

	height: INTEGER
			-- Vertical size in pixels.
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure then
			bridge_ok: Result = implementation.height
			positive: Result > 0

	width: INTEGER
			-- Horizontal size in pixels.
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure then
			bridge_ok: Result = implementation.width
			positive: Result > 0
	
feature -- Status report

	pointer_position: EV_COORDINATE
			-- Position of the screen pointer.
		require
			not_destroyed: not is_destroyed

	widget_at_position (x, y: INTEGER): EV_WIDGET
			-- Widget at position (x, y) if any.
		require
			not_destroyed: not is_destroyed
	
feature -- Status setting

	set_default_colors
			-- Set foreground and background color to their default values.
			-- (from EV_COLORIZABLE)
		require -- from EV_COLORIZABLE
			not_destroyed: not is_destroyed
	
feature -- Element change

	disable_dashed_line_style
			-- Draw lines solid.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			dashed_line_style_disabled: not dashed_line_style

	enable_dashed_line_style
			-- Draw lines dashed.
			-- See note at top.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			dashed_line_style_enabled: dashed_line_style

	remove_clip_area
			-- Do not apply any clipping.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			clip_area_void: clip_area = void

	remove_tile
			-- Do not apply a tile when filling.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			tile_void: tile = void

	set_background_color (a_color: like background_color)
			-- Assign a_color to foreground_color.
			-- (from EV_COLORIZABLE)
		require -- from EV_COLORIZABLE
			not_destroyed: not is_destroyed
			a_color_not_void: a_color /= void
		ensure -- from EV_COLORIZABLE
			background_color_assigned: background_color.is_equal (a_color)

	set_clip_area (an_area: EV_RECTANGLE)
			-- Set area which will be refreshed.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			an_area_not_void: an_area /= void
		ensure -- from EV_DRAWABLE
			clip_area_assigned: clip_area.is_equal (an_area)

	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

	set_drawing_mode (a_mode: INTEGER)
			-- Set drawing mode to a_logical_mode.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_mode_valid: valid_drawing_mode (a_mode)
		ensure -- from EV_DRAWABLE
			drawing_mode_assigned: drawing_mode = a_mode

	set_font (a_font: EV_FONT)
			-- Assign a_font to font.
			-- (from EV_FONTABLE)
		require -- from EV_FONTABLE
			not_destroyed: not is_destroyed
			a_font_not_void: a_font /= void
		ensure -- from EV_FONTABLE
			font_assigned: font.is_equal (a_font)

	set_foreground_color (a_color: like foreground_color)
			-- Assign a_color to foreground_color.
			-- (from EV_COLORIZABLE)
		require -- from EV_COLORIZABLE
			not_destroyed: not is_destroyed
			a_color_not_void: a_color /= void
		ensure -- from EV_COLORIZABLE
			foreground_color_assigned: foreground_color.is_equal (a_color)

	set_line_width (a_width: INTEGER)
			-- Assign a_width to line_width.
			-- See note at top.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_width_positive_or_zero: a_width >= 0
		ensure -- from EV_DRAWABLE
			line_width_assigned: line_width = a_width

	set_tile (a_pixmap: EV_PIXMAP)
			-- Set tile used to fill figures.
			-- Set to Void to use background_color to fill.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_pixmap_not_void: a_pixmap /= void
		ensure -- from EV_DRAWABLE
			tile_assigned: tile /= void
	
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 -- Basic operation

	fake_key_click (a_key: EV_KEY)
			-- Simulate the user clicking a key.
		require
			not_destroyed: not is_destroyed

	fake_key_press (a_key: EV_KEY)
			-- Simulate the user pressing a key.
		require
			not_destroyed: not is_destroyed

	fake_key_release (a_key: EV_KEY)
			-- Simulate the user releasing a key.
		require
			not_destroyed: not is_destroyed

	fake_pointer_button_click (a_button: INTEGER)
			-- Simulate the user clicking a_button on the pointing device.
		require
			not_destroyed: not is_destroyed

	fake_pointer_button_press (a_button: INTEGER)
			-- Simulate the user pressing a a_button on the pointing device.
		require
			not_destroyed: not is_destroyed

	fake_pointer_button_release (a_button: INTEGER)
			-- Simulate the user releasing a a_button on the pointing device.
		require
			not_destroyed: not is_destroyed

	set_pointer_position (x, y: INTEGER)
			-- Set pointer_position to (x,`y`).
		require
			not_destroyed: not is_destroyed
	
feature -- Clearing operations

	clear
			-- Erase Current with background_color.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed

	clear_rectangle (x, y, a_width, a_height: INTEGER)
			-- Draw rectangle with upper-left corner on (x, y)
			-- with size a_width and a_height in background_color.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_width_positive_or_zero: a_width >= 0
			a_height_positive_or_zero: a_height >= 0
	
feature -- Command

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

	valid_drawing_mode (a_mode: INTEGER): BOOLEAN
			-- Is a_mode a valid drawing mode?
			-- (from EV_DRAWABLE_CONSTANTS)
	
feature -- Drawing mode setting

	set_and_mode
			-- Set drawing_mode to bitwise AND.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			drawing_mode_assigned: drawing_mode = drawing_mode_and

	set_copy_mode
			-- Set drawing_mode to normal.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			drawing_mode_assigned: drawing_mode = drawing_mode_copy

	set_invert_mode
			-- Set drawing_mode to bitwise invert.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			drawing_mode_assigned: drawing_mode = drawing_mode_invert

	set_or_mode
			-- Set drawing_mode to bitwise OR.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			drawing_mode_assigned: drawing_mode = drawing_mode_or

	set_xor_mode
			-- Set drawing_mode to bitwise XOR.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
		ensure -- from EV_DRAWABLE
			drawing_mode_assigned: drawing_mode = drawing_mode_xor
	
feature -- Drawing operations

	draw_arc (x, y, a_bounding_width, a_bounding_height: INTEGER; a_start_angle, an_aperture: REAL)
			-- Draw part of an ellipse defined by a rectangular area with an
			-- upper left corner at x,y, width a_bounding_width and height
			-- a_bounding_height.
			-- Start at a_start_angle and stop at a_start_angle + an_aperture.
			-- Angles are measured in radians, and go
			-- counterclockwise from the 3 o'clock angle.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_bounding_width_positive_or_zero: a_bounding_width >= 0
			a_bounding_height_positive_or_zero: a_bounding_width >= 0

	draw_ellipse (x, y, a_bounding_width, a_bounding_height: INTEGER)
			-- Draw an ellipse defined by a rectangular area with an
			-- upper left corner at x,y, width a_bounding_width and height
			-- a_bounding_height.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_bounding_width_positive_or_zero: a_bounding_width >= 0
			a_bounding_height_positive_or_zero: a_bounding_height >= 0

	draw_pie_slice (x, y, a_bounding_width, a_bounding_height: INTEGER; a_start_angle, an_aperture: REAL)
			-- Draw part of an ellipse defined by a rectangular area with an
			-- upper left corner at x,y, width a_bounding_width and height
			-- a_bounding_height.
			-- Start at a_start_angle and stop at a_start_angle + an_aperture.
			-- The arc is then closed by two segments through (x, 'y').
			-- Angles are measured in radians, start at the
			-- 3 o'clock angle and grow counterclockwise.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_bounding_width_positive_or_zero: a_bounding_width >= 0
			a_bounding_height_positive_or_zero: a_bounding_height >= 0

	draw_pixmap (x, y: INTEGER; a_pixmap: EV_PIXMAP)
			-- Draw a_pixmap with upper-left corner on (x, y).
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_pixmap_not_void: a_pixmap /= void

	draw_point (x, y: INTEGER)
			-- Draw point at (x, y).
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed

	draw_polyline (points: ARRAY [EV_COORDINATE]; is_closed: BOOLEAN)
			-- Draw line segments between subsequent points in
			-- points. If is_closed draw line segment between first
			-- and last point in points.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			points_not_void: points /= void

	draw_rectangle (x, y, a_width, a_height: INTEGER)
			-- Draw rectangle with upper-left corner on (x, y)
			-- with size a_width and a_height.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_width_positive_or_zero: a_width >= 0
			a_height_positive_or_zero: a_height >= 0

	draw_segment (x1, y1, x2, y2: INTEGER)
			-- Draw line segment from (x1, y1) to (x2, y2).
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed

	draw_straight_line (x1, y1, x2, y2: INTEGER)
			-- Draw infinite straight line through (x1, y1) and
			-- (x2, y2).
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed

	draw_sub_pixmap (x, y: INTEGER; a_pixmap: EV_PIXMAP; area: EV_RECTANGLE)
			-- Draw area of a_pixmap with upper-left corner on (x, y).
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_pixmap_not_void: a_pixmap /= void
			area_not_void: area /= void

	draw_text (x, y: INTEGER; a_text: STRING)
			-- Draw a_text with left of baseline at (x, y) using font.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_text_not_void: a_text /= void

	draw_text_top_left (x, y: INTEGER; a_text: STRING)
			-- Draw a_text with top left corner at (x, y) using font.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_text_not_void: a_text /= void
	
feature -- Drawing operations (filled)

	fill_ellipse (x, y, a_bounding_width, a_bounding_height: INTEGER)
			-- Fill an ellipse defined by a rectangular area with an
			-- upper left corner at x,y, width a_bounding_width and height
			-- a_bounding_height.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_bounding_width_positive_or_zero: a_bounding_width >= 0
			a_bounding_height_positive_or_zero: a_bounding_height >= 0

	fill_pie_slice (x, y, a_bounding_width, a_bounding_height: INTEGER; a_start_angle, an_aperture: REAL)
			-- Fill part of an ellipse defined by a rectangular area with an
			-- upper left corner at x,y, width a_bounding_width and height
			-- a_bounding_height.
			-- Start at a_start_angle and stop at a_start_angle + an_aperture.
			-- The arc is then closed by two segments through (x, 'y').
			-- Angles are measured in radians, start at the 3
			-- o'clock angle and grow counterclockwise.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_bounding_width_positive_or_zero: a_bounding_width >= 0
			a_bounding_height_positive_or_zero: a_bounding_height >= 0

	fill_polygon (points: ARRAY [EV_COORDINATE])
			-- Draw filled polygon between subsequent points in points.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			points_not_void: points /= void

	fill_rectangle (x, y, a_width, a_height: INTEGER)
			-- Draw filled rectangle with upper-left corner on (x, y)
			-- with size a_width and a_height.
			-- (from EV_DRAWABLE)
		require -- from EV_DRAWABLE
			not_destroyed: not is_destroyed
			a_width_positive_or_zero: a_width >= 0
			a_height_positive_or_zero: a_height >= 0
	
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

	pointer_position_not_negative: pointer_position.x >= 0 and pointer_position.y >= 0
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from EV_DRAWABLE
	line_width_positive_or_zero: is_usable implies line_width >= 0
	drawing_mode_valid: is_usable implies valid_drawing_mode (drawing_mode)
		-- from EV_ANY
	is_initialized: is_initialized
	is_coupled: implementation /= void and then implementation.interface = Current
	default_create_called: default_create_called
		-- from EV_COLORIZABLE
	background_color_not_void: is_usable implies background_color /= void
	foreground_color_not_void: is_usable implies foreground_color /= void

end -- class EV_SCREEN