class interface WIN_SPEC
creation
make
-- Smalleiffel
feature(s) from WINDOW
-- Window public attributes
parent: OVERLAPPED_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, in screen coordinates
-- for an overlapped window.
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 OVERLAPPED_WINDOW
-- Actions: iconisation.
maximize
-- Maximise (show full screen) the window.
require
valid: is_valid
ensure
not_iconic: is_iconic = false
minimize
-- Minimise (reduce to an icon) the window.
require
valid: is_valid
ensure
iconic: is_iconic
restore
-- Show the window and restore to its normal size if
-- previously minimised or maximised.
require
valid: is_valid
feature(s) from OVERLAPPED_WINDOW
-- Keyboard accelerators
apply_accelerators
-- Apply keyboard accelerators for items of menus CURRENTLY
-- associated with this window, it should be called after the
-- menu system has been set up to enable keyboard shortcuts.
-- WARNING: If the menus are updated (or at least items with
-- associated accelerators are added or removed), this procedure
-- should be called again to update the table maintained by
-- the system.
require
valid: is_valid
feature(s) from DIALOG
-- Default dialog font used by all controls
set_font (ft: FONT)
-- Set default font.
require
valid: ft /= Void
ensure
keep_reference: font = ft
feature(s) from DIALOG
-- Action(s)
apply
-- Apply the dialog box settings.
finish
-- End processing.
feature(s) from DIALOG
-- Buttons & keyboard interface
set_ok_push_button (pushb: PUSH_BUTTON)
-- Set the button which is a default push button at
-- initialisation or when no other button is active.
-- will execute that button, which has to do
-- the actual action, such as calling 'apply' &
-- finish itself, like, for instance, OK_BUTTON.
require
ok: pushb /= Void
ensure
keep_reference: ok_push_button = pushb
set_cancel_push_button (pushb: PUSH_BUTTON)
-- Set the button which will be executed when is
-- pressed. The button is responsible for closing the
-- dialog, without applying the settings. CANCEL_BUTTON
-- provides an implementation of such a button.
require
ok: pushb /= Void
ensure
keep_reference: cancel_push_button = pushb
feature(s) from MODELESS_DIALOG
-- Creation
dialog_make (p: like parent)
-- Make dialog box with thick border.
require
valid: p /= Void
make_thin (p: like parent)
-- Make dialog box with thin border.
require
valid: p /= Void
feature(s) from MODELESS_DIALOG
-- Other actions
arrange
-- Resize nicely so that the box is at the centre of the parent window
-- and encloses all controls.
feature(s) from WIN_SPEC
-- Modal dialog implentation for type hole
when_prepared
-- Dialog is about to be displayed.
when_applied
-- Apply settings.
when_finished
-- Dialog has been closed.
end of WIN_SPEC