add support for paddings

This commit is contained in:
Fabian Jakobs 2010-11-02 16:54:04 +01:00
commit 729a8848d3

View file

@ -84,10 +84,11 @@ var VirtualRenderer = function(container, theme) {
scrollerWidth: 0
};
this.$updatePrintMargin();
this.$loop = new RenderLoop(lang.bind(this.$renderChanges, this));
this.$loop.schedule(this.CHANGE_FULL);
this.$updatePrintMargin();
this.setPadding(4);
};
(function() {
@ -283,12 +284,19 @@ var VirtualRenderer = function(container, theme) {
return (this.layerConfig || {}).lastRow || 0;
};
this.$padding = null;
this.setPadding = function(padding) {
this.$padding = padding;
this.content.style.padding = "0 " + padding + "px";
this.$loop.schedule(this.CHANGE_FULL);
};
this.onScroll = function(e) {
this.scrollToY(e.data);
};
this.$updateScrollBar = function() {
this.scrollBar.setInnerHeight(this.doc.getLength() * this.lineHeight);
this.scrollBar.setInnerHeight(this.doc.getLength() * this.lineHeight + this.$padding * 2);
this.scrollBar.setScrollTop(this.scrollTop);
};
@ -361,7 +369,7 @@ var VirtualRenderer = function(container, theme) {
};
this.$computeLayerConfig = function() {
var offset = this.scrollTop % this.lineHeight;
var offset = (this.scrollTop % this.lineHeight) - this.$padding;
var minHeight = this.$size.scrollerHeight + this.lineHeight;
var longestLine = this.$getLongestLine();
@ -373,6 +381,7 @@ var VirtualRenderer = function(container, theme) {
var layerConfig = this.layerConfig = {
width : longestLine,
padding : this.$padding,
firstRow : firstRow,
lastRow : lastRow,
lineHeight : this.lineHeight,
@ -392,6 +401,7 @@ var VirtualRenderer = function(container, theme) {
this.$gutterLayer.element.style.marginTop = (-offset) + "px";
this.content.style.marginTop = (-offset) + "px";
this.content.style.width = longestLine + "px";
this.content.style.height = minHeight + "px";
};
@ -428,7 +438,7 @@ var VirtualRenderer = function(container, theme) {
if (this.$showInvisibles)
charCount += 1;
return Math.max(this.$size.scrollerWidth, Math.round(charCount * this.characterWidth));
return Math.max(this.$size.scrollerWidth - this.$padding * 2, Math.round(charCount * this.characterWidth));
};
this.addMarker = function(range, clazz, type) {
@ -473,8 +483,8 @@ var VirtualRenderer = function(container, theme) {
this.scrollCursorIntoView = function() {
var pos = this.$cursorLayer.getPixelPosition();
var left = pos.left;
var top = pos.top;
var left = pos.left + this.$padding;
var top = pos.top + this.$padding;
if (this.getScrollTop() > top) {
this.scrollToY(top);
@ -486,13 +496,13 @@ var VirtualRenderer = function(container, theme) {
}
if (this.scroller.scrollLeft > left) {
this.scroller.scrollLeft = left;
this.scrollToX(left);
}
if (this.scroller.scrollLeft + this.$size.scrollerWidth < left
+ this.characterWidth) {
this.scroller.scrollLeft = Math.round(left + this.characterWidth
- this.$size.scrollerWidth);
this.scrollToX(Math.round(left + this.characterWidth
- this.$size.scrollerWidth));
}
},
@ -513,26 +523,37 @@ var VirtualRenderer = function(container, theme) {
};
this.scrollToY = function(scrollTop) {
var maxHeight = this.lines.length * this.lineHeight - this.$size.scrollerHeight;
var maxHeight = this.lines.length * this.lineHeight - this.$size.scrollerHeight + this.$padding * 2;
var scrollTop = Math.max(0, Math.min(maxHeight, scrollTop));
if (scrollTop >= maxHeight - this.$padding)
scrollTop = maxHeight;
else if (scrollTop <= this.$padding)
scrollTop = 0;
if (this.scrollTop !== scrollTop) {
this.scrollTop = scrollTop;
this.$loop.schedule(this.CHANGE_SCROLL);
}
};
this.scrollToX = function(scrollLeft) {
if (scrollLeft <= this.$padding)
scrollLeft = 0;
this.scroller.scrollLeft = scrollLeft;
};
this.scrollBy = function(deltaX, deltaY) {
deltaY && this.scrollToY(this.scrollTop + deltaY);
deltaX && (this.scroller.scrollLeft += deltaX);
deltaX && this.scrollToX(this.scroller.scrollLeft + deltaX);
};
this.screenToTextCoordinates = function(pageX, pageY) {
var canvasPos = this.scroller.getBoundingClientRect();
var col = Math.round((pageX + this.scroller.scrollLeft - canvasPos.left)
var col = Math.round((pageX + this.scroller.scrollLeft - canvasPos.left - this.$padding)
/ this.characterWidth);
var row = Math.floor((pageY + this.scrollTop - canvasPos.top)
var row = Math.floor((pageY + this.scrollTop - canvasPos.top - this.$padding)
/ this.lineHeight);
return {
@ -544,7 +565,7 @@ var VirtualRenderer = function(container, theme) {
this.textToScreenCoordinates = function(row, column) {
var canvasPos = this.scroller.getBoundingClientRect();
var x = Math.round(this.doc.documentToScreenColumn(row, column) * this.characterWidth);
var x = this.padding + Math.round(this.doc.documentToScreenColumn(row, column) * this.characterWidth);
var y = row * this.lineHeight;
return {
@ -602,4 +623,4 @@ var VirtualRenderer = function(container, theme) {
}).call(VirtualRenderer.prototype);
return VirtualRenderer;
});
});