deferred class interface DIALOG_SCROLLBAR
feature(s) from DIALOG_ELEMENT
-- Parent
has_dialog_box: BOOLEAN
-- Does the object has a valid corresponding dialog?
dialog_box: DIALOG
-- The object which uses dialog elements.
require
has_dialog: has_dialog_box
ensure
valid: Result /= Void
feature(s) from DIALOG_ELEMENT
-- Device independent positioning
indep_size: RECTANGLE
-- Size of element using device independent coordinates.
ensure
is_copy: -- can be modified.
indep_set_size (r: RECTANGLE)
-- Set element's size in device independent coordinates.
require
valid: r /= Void
ensure
done: r.is_equal(indep_size)
indep_set_point (p: POINT)
-- Set upper-left point of element using device independent units.
require
valid_point: p /= Void
indep_set_width (wi: INTEGER)
-- Set element's width using device independent units.
require
valid: wi >= 0
indep_set_height (he: INTEGER)
-- Set element's height using device independent units.
require
valid: he >= 0
feature(s) from DIALOG_ELEMENT
-- Relative positioning
place_right (other: DIALOG_ELEMENT)
-- Place the current element to the right of other.
require
valid_other: other /= Void
place_left (other: DIALOG_ELEMENT)
-- Place the current element to the left of other.
require
valid_other: other /= Void
place_above (other: DIALOG_ELEMENT)
-- Place the current element above other.
require
valid_other: other /= Void
place_under (other: DIALOG_ELEMENT)
-- Place the current element under other.
require
valid_other: other /= Void
place_just_under (other: DIALOG_ELEMENT)
-- Place the current element exactly under 'other'.
same_width (other: DIALOG_ELEMENT)
-- Set the current element width to other's.
require
valid_other: other /= Void
same_height (other: DIALOG_ELEMENT)
-- Set the current element height to be the same as other's.
require
valid_other: other /= Void
align_left (other: DIALOG_ELEMENT)
-- Align left side of this element with the
-- left side of other.
require
ok: other /= Void
align_right (other: DIALOG_ELEMENT)
-- Align the right side of this element with the right
-- side of other.
require
ok: other /= Void
align_top (other: DIALOG_ELEMENT)
-- Align the top of this element with top of other.
require
ok: other /= Void
align_bottom (other: DIALOG_ELEMENT)
-- Align the bottom of this element with bottom of other.
require
ok: other /= Void
feature(s) from SCROLLBAR
-- Type of scrollbar
is_horizontal: BOOLEAN
-- Is this scrollbar horizontal?
ensure
coherent: is_vertical = not is_horizontal
is_vertical: BOOLEAN
-- Is this scrollbar vertical?
ensure
coherent: is_vertical = not is_horizontal
feature(s) from SCROLLBAR
-- Range & conversion from/to ratios
Default_range: INTEGER
range: INTEGER
-- Slider position range.
set_range (rg: INTEGER)
-- Set slider position range.
ensure
ok: -- range = rg unless recursive size change
is_valid_range (r: INTEGER): BOOLEAN
-- Is the given range valid?
ensure
done: -- Result implies (r >= 1 and Result <= range)
units_to_ratio (unit: INTEGER): DOUBLE
-- Convert from 1-(INTEGER) to 0-1 (DOUBLE)
require
valid_range: is_valid_range(unit)
ensure
good_ratio: Result >= 0 and then Result <= 1
ratio_to_units (ratio: DOUBLE): INTEGER
-- Convert from 0-1 (DOUBLE) to 1-(INTEGER).
require
good_ratio: ratio >= 0 and then ratio <= 1
ensure
valid_range: is_valid_range(Result)
feature(s) from SCROLLBAR
-- Steppings
line_step: INTEGER
-- Step to go when line up/down.
page_step: INTEGER
-- Step to go when page up/down.
set_line_step (rg: INTEGER)
-- Set line_step.
require
positive: rg >= 0
set_page_step (rg: INTEGER)
-- Set page_step.
require
positive: rg >= 0
feature(s) from SCROLLBAR
-- Slider position and size
slider_size: INTEGER
-- Size of the slider, on a 1-range scale.
-- Note: some implementations only support square sliders.
set_slider_size (s: INTEGER)
-- Set the size of the slider on a 1-range scale.
-- Note: some implementations only support square sliders.
require
correct_size: is_valid_range(s)
ensure
size_set: slider_size = s
slider_position: INTEGER
-- Position of the slider on a 0-range scale.
ensure
is_valid_range(Result)
set_slider_position (pos: INTEGER)
-- Set the position of the slider on a 1-range scale.
require
correct_pos: is_valid_range(pos)
ensure
pos_set: pos = slider_position
feature(s) from SCROLLBAR
-- Event support
tracked: BOOLEAN
-- Is the mouse cursor currently moving slider.
feature(s) from SCROLLBAR
-- Command
set_command (gc: GUI_COMMAND)
-- Set when_slider_moved command.
require
nothing: -- Void is no command
invariant
valid_dir: is_horizontal xor is_vertical;
end of deferred DIALOG_SCROLLBAR