fix scrolling issues

This commit is contained in:
Fabian Jakobs 2011-12-21 16:16:19 +01:00
commit 827490fedd

View file

@ -242,7 +242,7 @@ var VirtualRenderer = function(container, theme) {
this.scrollBar.setHeight(size.scrollerHeight);
if (this.session) {
this.scrollToY(this.getScrollTop());
this.session.setScrollTop(this.getScrollTop());
changes = changes | this.CHANGE_FULL;
}
}
@ -641,11 +641,11 @@ var VirtualRenderer = function(container, theme) {
var top = pos.top;
if (this.scrollTop > top) {
this.scrollToY(top);
this.session.setScrollTop(top);
}
if (this.scrollTop + this.$size.scrollerHeight < top + this.lineHeight) {
this.scrollToY(top + this.lineHeight - this.$size.scrollerHeight);
this.session.setScrollTop(top + this.lineHeight - this.$size.scrollerHeight);
}
var scrollLeft = this.scrollLeft;
@ -681,7 +681,7 @@ var VirtualRenderer = function(container, theme) {
};
this.scrollToRow = function(row) {
this.scrollToY(row * this.lineHeight);
this.session.setScrollTop(row * this.lineHeight);
};
this.scrollToLine = function(line, center) {
@ -694,7 +694,7 @@ var VirtualRenderer = function(container, theme) {
if (center) {
offset -= this.$size.scrollerHeight / 2;
}
this.scrollToY(offset);
this.session.setScrollTop(offset);
};
this.scrollToY = function(scrollTop) {