fix jumping selections. Reverts most of 64a55719b2

This commit is contained in:
Fabian Jakobs 2011-06-07 17:41:14 +02:00
commit 9b662c998f

View file

@ -95,7 +95,7 @@ var VirtualRenderer = function(container, theme) {
this.scrollBar = new ScrollBar(container); this.scrollBar = new ScrollBar(container);
this.scrollBar.addEventListener("scroll", this.onScroll.bind(this)); this.scrollBar.addEventListener("scroll", this.onScroll.bind(this));
this.scrollTop = this.desiredScrollTop = 0; this.scrollTop = 0;
this.cursorPos = { this.cursorPos = {
row : 0, row : 0,
@ -470,8 +470,7 @@ var VirtualRenderer = function(container, theme) {
this.scroller.style.overflowX = horizScroll ? "scroll" : "hidden"; this.scroller.style.overflowX = horizScroll ? "scroll" : "hidden";
var maxHeight = this.session.getScreenLength() * this.lineHeight; var maxHeight = this.session.getScreenLength() * this.lineHeight;
this.scrollTop = this.desiredScrollTop = this.scrollTop = Math.max(0, Math.min(this.scrollTop, maxHeight - this.$size.scrollerHeight));
Math.max(0, Math.min(this.desiredScrollTop, maxHeight - this.$size.scrollerHeight));
var lineCount = Math.ceil(minHeight / this.lineHeight) - 1; var lineCount = Math.ceil(minHeight / this.lineHeight) - 1;
var firstRow = Math.max(0, Math.round((this.scrollTop - offset) / this.lineHeight)); var firstRow = Math.max(0, Math.round((this.scrollTop - offset) / this.lineHeight));
@ -617,11 +616,11 @@ var VirtualRenderer = function(container, theme) {
var left = pos.left + this.$padding; var left = pos.left + this.$padding;
var top = pos.top; var top = pos.top;
if (this.desiredScrollTop > top) { if (this.scrollTop > top) {
this.scrollToY(top); this.scrollToY(top);
} }
if (this.desiredScrollTop + this.$size.scrollerHeight < top + this.lineHeight) { if (this.scrollTop + this.$size.scrollerHeight < top + this.lineHeight) {
this.scrollToY(top + this.lineHeight - this.$size.scrollerHeight); this.scrollToY(top + this.lineHeight - this.$size.scrollerHeight);
} }
@ -675,9 +674,10 @@ var VirtualRenderer = function(container, theme) {
this.scrollToY = function(scrollTop) { this.scrollToY = function(scrollTop) {
// after calling scrollBar.setScrollTop // after calling scrollBar.setScrollTop
// scrollbar sends us event with same scrollTop. ignore it // scrollbar sends us event with same scrollTop. ignore it
if (this.desiredScrollTop !== scrollTop) { scrollTop = Math.max(0, scrollTop);
if (this.scrollTop !== scrollTop) {
this.$loop.schedule(this.CHANGE_SCROLL); this.$loop.schedule(this.CHANGE_SCROLL);
this.desiredScrollTop = scrollTop; this.scrollTop = scrollTop;
} }
}; };