fix scrolling error widget into view
This commit is contained in:
parent
f3af20aa15
commit
36c6fcc9d4
2 changed files with 11 additions and 8 deletions
|
|
@ -171,6 +171,8 @@ exports.showErrorMarker = function(editor, dir) {
|
||||||
editor.session.widgetManager.addLineWidget(w);
|
editor.session.widgetManager.addLineWidget(w);
|
||||||
|
|
||||||
w.el.onmousedown = editor.focus.bind(editor);
|
w.el.onmousedown = editor.focus.bind(editor);
|
||||||
|
|
||||||
|
editor.renderer.scrollCursorIntoView(null, 0.5, {bottom: w.el.offsetHeight});
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1114,7 +1114,7 @@ var VirtualRenderer = function(container, theme) {
|
||||||
*
|
*
|
||||||
* Scrolls the cursor into the first visibile area of the editor
|
* Scrolls the cursor into the first visibile area of the editor
|
||||||
**/
|
**/
|
||||||
this.scrollCursorIntoView = function(cursor, offset) {
|
this.scrollCursorIntoView = function(cursor, offset, $viewMargin) {
|
||||||
// the editor is not visible
|
// the editor is not visible
|
||||||
if (this.$size.scrollerHeight === 0)
|
if (this.$size.scrollerHeight === 0)
|
||||||
return;
|
return;
|
||||||
|
|
@ -1124,17 +1124,18 @@ var VirtualRenderer = function(container, theme) {
|
||||||
var left = pos.left;
|
var left = pos.left;
|
||||||
var top = pos.top;
|
var top = pos.top;
|
||||||
|
|
||||||
|
var topMargin = $viewMargin && $viewMargin.top || 0;
|
||||||
|
var bottomMargin = $viewMargin && $viewMargin.bottom || 0;
|
||||||
|
|
||||||
var scrollTop = this.$scrollAnimation ? this.session.getScrollTop() : this.scrollTop;
|
var scrollTop = this.$scrollAnimation ? this.session.getScrollTop() : this.scrollTop;
|
||||||
|
|
||||||
if (scrollTop > top) {
|
if (scrollTop + topMargin > top) {
|
||||||
if (offset)
|
if (offset)
|
||||||
top -= offset * this.$size.scrollerHeight;
|
top -= offset * this.$size.scrollerHeight;
|
||||||
if (top == 0)
|
if (top === 0)
|
||||||
top = - this.scrollMargin.top;
|
top = -this.scrollMargin.top;
|
||||||
else if (top == 0)
|
|
||||||
top = + this.scrollMargin.bottom;
|
|
||||||
this.session.setScrollTop(top);
|
this.session.setScrollTop(top);
|
||||||
} else if (scrollTop + this.$size.scrollerHeight < top + this.lineHeight) {
|
} else if (scrollTop + this.$size.scrollerHeight - bottomMargin < top + this.lineHeight) {
|
||||||
if (offset)
|
if (offset)
|
||||||
top += offset * this.$size.scrollerHeight;
|
top += offset * this.$size.scrollerHeight;
|
||||||
this.session.setScrollTop(top + this.lineHeight - this.$size.scrollerHeight);
|
this.session.setScrollTop(top + this.lineHeight - this.$size.scrollerHeight);
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue