class interface SPLIT_WINDOW
creation
make_horizontal (p: like parent)
-- Create horizontal split window.
make_vertical (p: like parent)
-- Create vertical split window.
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 CHILD_WINDOW_CURSOR
-- Cursor
set_cursor (mc: MOUSE_CURSOR)
-- Change this window's cursor.
require
ok: mc /= Void and mc.is_valid
ensure
keep_reference: cursor = mc
feature(s) from P_TEXT_OBJECT
-- Public interface
to_string: STRING
ensure
is_copy: Result /= Void
from_string (str: STRING)
-- Init object from string.
require
valid: str /= Void
ensure
done: -- success implies to_string.is_equal(str)
feature(s) from SPLIT_WINDOW
-- Setup
set_first (win: CHILD_WINDOW)
-- Set right or top window.
require
ok: win /= Void;
child: win.parent = Current
ensure
keep_reference: first = win
set_second (win: CHILD_WINDOW)
-- Set left or bottom window.
require
ok: win /= Void;
child: win.parent = Current
ensure
keep_reference: second = win
set_split (newsplit: DOUBLE)
-- Set split bar position.
require
ok: newsplit >= 0 and newsplit <= 1
invariant
has_parent: parent /= Void; -- hscroll: has_horizontal_scrollbar implies horizontal_scrollbar /= Void
-- vscroll: has_horizontal_scrollbar implies vertical_scrollbar /= Void
split: split >= 0;
end of SPLIT_WINDOW