class interface GRAPHICS
creation
make (p: WINDOW)
make_child (par: like parent)
-- Create a child window.
require
valid: par /= Void and then par.is_valid
ensure
keep_reference: par = parent
feature(s) from WINDOW
-- Window public attributes
parent: WINDOW
-- Parent window, it may be redefined by heirs in order to
-- communicate with parent window.
feature(s) from WINDOW
-- Graphic device
device: WINDOW_DEVICE
-- Device used to draw in the window client area.
ensure
has_device: Result /= Void
feature(s) from WINDOW
-- Window's size
size: RECTANGLE
-- Return the window external size relative to the client area
-- of the parent window for child windows.
require
valid: is_valid
ensure
valid_result: Result /= Void; -- can be modified
is_copy:
client_size: RECTANGLE
-- Return the window's client area size, in client
-- coordinates, that is (x, y) = (0, 0)
require
valid: is_valid
ensure
is_copy: Result /= Void; -- can be modified
-- Result.lower.is_origin
lower_zero:
set_size (rect: RECTANGLE)
-- Set window size. The rectangle is in screen coordinates
-- for a popup windown and in the parent's window client area
-- coordinates for a child window.
require
valid_window: is_valid;
valid_rect: rect /= Void
ensure
size_set: rect.is_equal(size)
set_client_size (rect: RECTANGLE)
-- Set the client area size, in client area coordinates
-- (so, (x, y) = (0, 0))
require
valid_window: is_valid;
valid_rect: rect /= Void;
lower_zero: rect.lower.x = 0 and rect.lower.y = 0
ensure
size_set: rect.is_equal(client_size)
feature(s) from WINDOW
-- Window's text
text: STRING
-- Get the window text, which can be the title bar for windows
-- with a caption, or used for other purposes.
require
valid: is_valid
ensure
is_copy: -- can be modified
set_text (s: STRING)
-- Set the window text (see 'text').
require
valid_window: is_valid;
valid_string: s /= Void
ensure
text_set: s.is_equal(text)
feature(s) from WINDOW
-- Associated mouse managers
set_left_mouse_manager (track: MOUSE_HANDLER)
-- Set associated mouse manager object for left mouse button.
require
void: -- track = Void implies no tracker
ensure
keep_reference: lmousetrack = track -- keeps a copy of track
set_right_mouse_manager (track: MOUSE_HANDLER)
-- Set associated mouse manager object for right mouse button.
-- (Default: none)
require
void: -- track = Void implies no tracker
ensure
keep_reference: rmousetrack = track -- keeps a copy of track
feature(s) from WINDOW
-- Window features and metrics
is_valid: BOOLEAN
-- Is this window currently valid? If not it has been closed
-- or failed to be created properly.
is_iconic: BOOLEAN
-- Is this window reduced to an icon?
require
valid: is_valid
is_enabled: BOOLEAN
-- Is the window able to receive user input?
require
valid: is_valid
has_focus: BOOLEAN
-- Does the window has the keyboard focus?
require
valid: is_valid
is_active: BOOLEAN
-- Is the window active?
require
valid: is_valid
is_visible: BOOLEAN
-- Is the window visible?
require
valid: is_valid
is_created: BOOLEAN
-- Has this window been created?
feature(s) from WINDOW
-- Close status
is_close_ready: BOOLEAN
-- Is the window ready to be closed.
-- If true, calling close or a close message will
-- destroy the window. (Default value: true)
set_close_ready (cl: BOOLEAN)
-- Set is_close_ready.
ensure
is_close_ready = cl
feature(s) from WINDOW
-- Actions: destruction
close
-- Close the window, and then destroy it if
-- is_close_ready is true.
require
valid: is_valid
destroy
-- Destroy the window (without calling 'when_closed').
require
valid: is_valid
ensure
invalid: -- not is_valid after when_destroyed
feature(s) from WINDOW
-- Actions: change the way the window is displayed
show
-- Show the window and redraw its client area.
-- Can be used to unhide, or restore a window.
require
valid: is_valid
ensure
visible: -- is_visible unless not parent.is_visible
hide
-- Hide the window (unhide with show).
require
valid: is_valid
ensure
hidden: not is_visible
feature(s) from WINDOW
-- Actions: activation, focus, etc
activate
-- Activate the current window (make it top).
require
valid: is_valid
ensure
active: is_active
focus
-- Set keyboard focus to this window.
require
valid: is_valid
ensure
focus: -- has_focus unless immediatly given to someone else
enable
-- Allow the user to use the window.
require
valid: is_valid
ensure
enabled: is_enabled = true
disable
-- Prevent the user from using the window.
require
valid: is_valid
ensure
disabled: is_enabled = false
feature(s) from WINDOW
-- Painting the window
paint
-- Force a redraw of the client area of the window.
require
valid: is_valid
paint_rectangle (rect: RECTANGLE)
-- Force a redraw of the specified rectangle of the client area.
require
valid_window: is_valid;
valid_rectangle: rect /= Void
horizontal_scroll (dx: INTEGER)
-- Scroll horizontally the client area of the window of 'dx',
-- and repaint the scrolled part.
require
valid: is_valid
vertical_scroll (dy: INTEGER)
-- Scroll vertically the client area of the window of 'dy',
-- and repaint the scrolled part.
require
valid: is_valid
feature(s) from CHILD_WINDOW
-- Attached scrollbars
horizontal_scrollbar: WINDOW_SCROLLBAR
vertical_scrollbar: WINDOW_SCROLLBAR
feature(s) from CHILD_WINDOW
-- Style
set_border (hasborder: BOOLEAN)
-- Set the window's border style:
-- hasborder = true implies one pixel border, otherwise not.
require
valid: is_valid
feature(s) from CHILD_WINDOW
-- Siblings
is_sibling (other: WINDOW): BOOLEAN
-- Is other an _older_ sibling of us?
-- (exported for preconditions)
require
valid_window: other /= Void;
has_parent: parent /= Void
next: CHILD_WINDOW
-- Next sibling in the cycle (may be Current).
previous: CHILD_WINDOW
-- Previous sibling in the cycle (may be Current).
feature(s) from CHILD_WINDOW
-- Setting up resize rules
size_follows_parent
-- Child window fills parent client area.
fixed_width
-- Width remains constant when layout changed.
require
valid: is_valid
fixed_height
-- Height remains constant when layout changed.
require
valid: is_valid
feature(s) from DEMO_CHILD
popup: POPUP_MENU
-- Menu associated with this window.
make_popup (par: OVERLAPPED_WINDOW)
-- Initialise 'popup'.
ensure
done: popup /= Void
feature(s) from GUI_COMMAND
heart_beat
-- Command
feature(s) from GRAPHICS
set_figure (fig: GRAPHICS_COMMAND)
require
ok: fig /= Void
feature(s) from GRAPHICS
when_created
-- Window created, but not yet displayed. This is the first
-- event.
require
not_created: not is_created
ensure
created: -- system sets is_created to true after this event.
when_closed
-- Window is going to be closed. (if is_closed_ready = true)
when_drawn
-- Window content is to be drawn.
require
device_ok: -- device.is_ready
invariant
has_parent: parent /= Void; -- hscroll: has_horizontal_scrollbar implies horizontal_scrollbar /= Void
-- vscroll: has_horizontal_scrollbar implies vertical_scrollbar /= Void
end of GRAPHICS