deferred class interface GRAPHICS_COMMAND
feature(s) from GUI_COMMAND
execute
-- Event.
feature(s) from GRAPHICS_COMMAND
figure (pt: POINT; size: INTEGER): DRAWABLE
-- Produce drawable object.
require
ok: pt /= Void;
valid_size: size > 0
ensure
done: Result /= Void
end of deferred GRAPHICS_COMMAND