(x1, y1, x2, y2)
| 1093 | return scrollIntoView(x, cursor.y, x, cursor.yBot); |
| 1094 | } |
| 1095 | function scrollIntoView(x1, y1, x2, y2) { |
| 1096 | var pl = paddingLeft(), pt = paddingTop(); |
| 1097 | y1 += pt; y2 += pt; x1 += pl; x2 += pl; |
| 1098 | var screen = scroller.clientHeight, screentop = scroller.scrollTop, scrolled = false, result = true; |
| 1099 | if (y1 < screentop) {scroller.scrollTop = Math.max(0, y1); scrolled = true;} |
| 1100 | else if (y2 > screentop + screen) {scroller.scrollTop = y2 - screen; scrolled = true;} |
| 1101 | |
| 1102 | var screenw = scroller.clientWidth, screenleft = scroller.scrollLeft; |
| 1103 | var gutterw = options.fixedGutter ? gutter.clientWidth : 0; |
| 1104 | var atLeft = x1 < gutterw + pl + 10; |
| 1105 | if (x1 < screenleft + gutterw || atLeft) { |
| 1106 | if (atLeft) x1 = 0; |
| 1107 | scroller.scrollLeft = Math.max(0, x1 - 10 - gutterw); |
| 1108 | scrolled = true; |
| 1109 | } |
| 1110 | else if (x2 > screenw + screenleft - 3) { |
| 1111 | scroller.scrollLeft = x2 + 10 - screenw; |
| 1112 | scrolled = true; |
| 1113 | if (x2 > code.clientWidth) result = false; |
| 1114 | } |
| 1115 | if (scrolled && options.onScroll) options.onScroll(instance); |
| 1116 | return result; |
| 1117 | } |
| 1118 | |
| 1119 | function visibleLines() { |
| 1120 | var lh = textHeight(), top = scroller.scrollTop - paddingTop(); |
no test coverage detected