class interface MOUSE_HANDLER
creation
make (win: like parent)
-- Create the mouse handler for one button.
ensure
down: not is_down and not dragging;
keep_reference: win = parent
feature(s) from MOUSE_HANDLER
-- Parent window
parent: WINDOW
-- Associated window.
feature(s) from MOUSE_HANDLER
-- Mouse button status
is_down: BOOLEAN
-- Is the button down?
point: POINT
-- Current position of the mouse pointer.
invariant
valid_point: point /= Void;
end of MOUSE_HANDLER