// set, the window is vertically scrolled to the top; otherwise, no
// scrolling is done. If <addToHist> is set, this page change is
// added to the history list.
// set, the window is vertically scrolled to the top; otherwise, no
// scrolling is done. If <addToHist> is set, this page change is
// added to the history list.