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

em.widget.border

Class EM_NO_BORDER


Direct ancestors

EM_BORDER

Features

Invariants

indexing

description

Implementation of an empty border to avoid a void reference in the widget.

date

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

revision

$Revision: 1.6 $

class

EM_NO_BORDER

inherit

EM_BORDER

feature -- Access

bottom: INTEGER

-- Bottom size of border

-- (From EM_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)

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

border_size_zero: top = 0 and left = 0 and right = 0 and bottom = 0

-- 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