class interface DRAWABLE_GUI_RECTANGLE
creation
make
-- Creation.
feature(s) from DRAWABLE_RECTANGLE
-- Position
set_position (rect: RECTANGLE)
-- Set rectangle to be drawn.
require
valid_rectangle: rect /= Void
ensure
done: position.is_equal(rect)
feature(s) from DRAWABLE_GUI_RECTANGLE
-- Type
set_type_invert
-- Filled xor-ed rectangle.
set_type_focus
-- Focus rectangle (dotted xor-ed frame).
set_type_normal
-- Default rectangle.
reset_type
-- Default rectangle.
invariant
valid_position: position /= Void;
end of DRAWABLE_GUI_RECTANGLE