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

em.widget.border

Class EM_LINE_BORDER


Direct ancestors

EM_BORDER

Creation

Features

Invariants

indexing

description

Line border with equal width on all sides and a fixed color.

date

$Date: 2005/10/23 11:12:24 $

revision

$Revision: 1.9 $

class

EM_LINE_BORDER

inherit

EM_BORDER

create

make (a_color: like color; a_width: like width)

-- Initialise Current with a_color and a_width.

require
a_color_not_void: a_color /= Void
a_width_not_negative: a_width >= 0
ensure
color_set: color = a_color
width_set: width = a_width

feature -- Access

bottom: INTEGER

-- Bottom size of border

-- (From EM_BORDER)

color: EM_COLOR

-- Color of border

left: INTEGER

-- Left size of border

-- (From EM_BORDER)

right: INTEGER

-- Right size of border

-- (From EM_BORDER)

top: INTEGER

-- Top size of border

-- (From EM_BORDER)

width: INTEGER

-- Width of border

feature -- Element change

set_color (a_color: like color)

-- Set color to a_color.

require
a_color_not_void: a_color /= Void
ensure
color_set: color = a_color
set_width (a_width: like width)

-- Set width to a_width.

require
a_width_not_negative: a_width >= 0
ensure
width_set: width = a_width

feature -- Drawing

draw_on (a_widget: EM_WIDGET)

-- Draw border on a_widget.

-- (From EM_BORDER)

require
a_widget_not_void: a_widget /= Void

invariant

width_not_negative: width >= 0
color_not_void: color /= Void

-- From EM_BORDER
non_negative_size: top >= 0 and left >= 0 and right >= 0 and bottom >= 0

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

end