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

em.widget.border

Class EM_BORDER


Known direct descendants

EM_NO_BORDER, EM_LINE_BORDER, EM_BEVEL_BORDER, EM_NAMED_BORDER

Features

Invariants

indexing

description

Border of an EM_WIDGET.

date

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

revision

$Revision: 1.7 $

deferred class

EM_BORDER

feature -- Access

bottom: INTEGER

-- Bottom size of border

left: INTEGER

-- Left size of border

right: INTEGER

-- Right size of border

top: INTEGER

-- Top size of border

feature -- Drawing

draw_on (a_widget: EM_WIDGET)

-- Draw border on a_widget.

require
a_widget_not_void: a_widget /= Void

invariant

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