Allow up to double the size for overview ruler decorations

Fixes #3840
This commit is contained in:
Daniel Imms
2022-05-27 11:56:54 -07:00
parent 1980f675f9
commit 7a652c4169
@@ -88,6 +88,7 @@ export class OverviewRulerRenderer extends Disposable {
}));
this.register(this._bufferService.onScroll(() => {
if (this._lastKnownBufferLength !== this._bufferService.buffers.normal.lines.length) {
this._refreshDrawHeightConstants();
this._refreshColorZonePadding();
}
}));
@@ -132,10 +133,7 @@ export class OverviewRulerRenderer extends Disposable {
drawWidth.center = innerWidth;
drawWidth.right = outerWidth;
// height
drawHeight.full = Math.round(2 * window.devicePixelRatio);
drawHeight.left = Math.round(6 * window.devicePixelRatio);
drawHeight.center = Math.round(6 * window.devicePixelRatio);
drawHeight.right = Math.round(6 * window.devicePixelRatio);
this._refreshDrawHeightConstants();
// x
drawX.full = 0;
drawX.left = 0;
@@ -143,6 +141,17 @@ export class OverviewRulerRenderer extends Disposable {
drawX.right = drawWidth.left + drawWidth.center;
}
private _refreshDrawHeightConstants(): void {
drawHeight.full = Math.round(2 * window.devicePixelRatio);
// Calculate actual pixels per line
const pixelsPerLine = this._canvas.height / this._bufferService.buffer.lines.length;
// Clamp actual pixels within a range
const nonFullHeight = Math.round(Math.max(Math.min(pixelsPerLine, 12), 6) * window.devicePixelRatio);
drawHeight.left = nonFullHeight;
drawHeight.center = nonFullHeight;
drawHeight.right = nonFullHeight;
}
private _refreshColorZonePadding(): void {
this._colorZoneStore.setPadding({
full: Math.floor(this._bufferService.buffers.active.lines.length / (this._canvas.height - 1) * drawHeight.full),