(cm, rect)
| 4838 | // If an editor sits on the top or bottom of the window, partially |
| 4839 | // scrolled out of view, this ensures that the cursor is visible. |
| 4840 | function maybeScrollWindow(cm, rect) { |
| 4841 | if (signalDOMEvent(cm, "scrollCursorIntoView")) { |
| 4842 | return |
| 4843 | } |
| 4844 | |
| 4845 | var display = cm.display, |
| 4846 | box = display.sizer.getBoundingClientRect(), |
| 4847 | doScroll = null |
| 4848 | if (rect.top + box.top < 0) { |
| 4849 | doScroll = true |
| 4850 | } else if (rect.bottom + box.top > (window.innerHeight || document.documentElement.clientHeight)) { |
| 4851 | doScroll = false |
| 4852 | } |
| 4853 | if (doScroll != null && !phantom) { |
| 4854 | var scrollNode = elt( |
| 4855 | "div", |
| 4856 | "\u200b", |
| 4857 | null, |
| 4858 | "position: absolute;\n top: " + |
| 4859 | (rect.top - display.viewOffset - paddingTop(cm.display)) + |
| 4860 | "px;\n height: " + |
| 4861 | (rect.bottom - rect.top + scrollGap(cm) + display.barHeight) + |
| 4862 | "px;\n left: " + |
| 4863 | rect.left + |
| 4864 | "px; width: " + |
| 4865 | Math.max(2, rect.right - rect.left) + |
| 4866 | "px;" |
| 4867 | ) |
| 4868 | cm.display.lineSpace.appendChild(scrollNode) |
| 4869 | scrollNode.scrollIntoView(doScroll) |
| 4870 | cm.display.lineSpace.removeChild(scrollNode) |
| 4871 | } |
| 4872 | } |
| 4873 | |
| 4874 | // Scroll a given position into view (immediately), verifying that |
| 4875 | // it actually became visible (as line heights are accurately |
no test coverage detected