class interface SPLIT_WINDOW_MOUSE
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 SPLIT_WINDOW_MOUSE