39 |
pixmap: EV_PIXMAP |
pixmap: EV_PIXMAP |
40 |
-- Icon for tool bar button representing `Current'. |
-- Icon for tool bar button representing `Current'. |
41 |
|
|
42 |
|
pixel_buffer: EV_PIXEL_BUFFER |
43 |
|
-- Icon for tool bar button representing `Current'. |
44 |
|
|
45 |
mini_pixmap: EV_PIXMAP |
mini_pixmap: EV_PIXMAP |
46 |
-- Icon for mini tool bar button representing `Current'. |
-- Icon for mini tool bar button representing `Current'. |
47 |
|
|
70 |
pixmap := new_p |
pixmap := new_p |
71 |
end |
end |
72 |
|
|
73 |
|
set_pixel_buffer (a_buffer: EV_PIXEL_BUFFER) is |
74 |
|
-- Define pixel buffer associated with `Current'. |
75 |
|
require |
76 |
|
a_buffer_not_void: a_buffer /= Void |
77 |
|
do |
78 |
|
pixel_buffer := a_buffer |
79 |
|
end |
80 |
|
|
81 |
set_tooltip (s: STRING) is |
set_tooltip (s: STRING) is |
82 |
-- Define a new tooltip for `Current', and possibly a new description. |
-- Define a new tooltip for `Current', and possibly a new description. |
83 |
do |
do |