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