indexing

	description: "[

		Border of an EM_WIDGET.

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

deferred class EM_BORDER

feature -- Access

	top: INTEGER
			-- Top size of border

	left: INTEGER
			-- Left size of border

	right: INTEGER
			-- Right size of border

	bottom: INTEGER
			-- Bottom size of border

feature -- Drawing

	draw_on (a_widget: EM_WIDGET) is
			-- Draw border on `a_widget'.
		require
			a_widget_not_void: a_widget /= Void
		deferred
		end

invariant

	non_negative_size: top >= 0 and left >= 0 and right >= 0 and bottom >= 0

end