diff options
| -rw-r--r-- | org.eclipse.jface.text/src/org/eclipse/jface/text/source/OverviewRuler.java | 18 | ||||
| -rw-r--r-- | org.eclipse.jface.text/src/org/eclipse/jface/text/source/SourceViewer.java | 28 |
2 files changed, 35 insertions, 11 deletions
diff --git a/org.eclipse.jface.text/src/org/eclipse/jface/text/source/OverviewRuler.java b/org.eclipse.jface.text/src/org/eclipse/jface/text/source/OverviewRuler.java index fca2c058d9f..1064840d8f2 100644 --- a/org.eclipse.jface.text/src/org/eclipse/jface/text/source/OverviewRuler.java +++ b/org.eclipse.jface.text/src/org/eclipse/jface/text/source/OverviewRuler.java @@ -347,7 +347,23 @@ public class OverviewRuler implements IOverviewRulerExtension, IOverviewRuler { writable= JFaceTextUtil.computeLineHeight(textWidget, 0, maxLines, maxLines); ScrollBar verticalBar= textWidget.getVerticalBar(); - thumbHeight= verticalBar != null ? Math.max(Math.min(bounds.height, verticalBar.getThumbBounds().height), 0) : 0; + if (verticalBar != null && !verticalBar.getVisible()) { + // Note: when the vertical bar is invisible, the thumbHeight is not reliable, + // so, we'll compute what would be the thumbHeight in case it was visible. + int max= verticalBar.getMaximum(); + double clientAreaHeight= textWidget.getClientArea().height; + if (max > clientAreaHeight) { + double percentage= clientAreaHeight / max; + thumbHeight= (int) (bounds.height * percentage); + } else { + thumbHeight= bounds.height; + } + if (thumbHeight < 0) { + thumbHeight= 0; + } + } else { + thumbHeight= verticalBar != null ? Math.max(Math.min(bounds.height, verticalBar.getThumbBounds().height), 0) : 0; + } int partialTopIndex= JFaceTextUtil.getPartialTopIndex(textWidget); int topLineHeight= textWidget.getLineHeight(textWidget.getOffsetAtLine(partialTopIndex)); diff --git a/org.eclipse.jface.text/src/org/eclipse/jface/text/source/SourceViewer.java b/org.eclipse.jface.text/src/org/eclipse/jface/text/source/SourceViewer.java index 99eb3f5766b..cab98611df1 100644 --- a/org.eclipse.jface.text/src/org/eclipse/jface/text/source/SourceViewer.java +++ b/org.eclipse.jface.text/src/org/eclipse/jface/text/source/SourceViewer.java @@ -136,12 +136,12 @@ public class SourceViewer extends TextViewer implements ISourceViewer, ISourceVi width -= overviewRulerWidth + fGap; } + ScrollBar horizontalBar= textWidget.getHorizontalBar(); + final boolean hScrollVisible= horizontalBar != null && horizontalBar.getVisible(); if (fVerticalRuler != null && fIsVerticalRulerVisible) { int verticalRulerWidth= fVerticalRuler.getWidth(); final Control verticalRulerControl= fVerticalRuler.getControl(); int oldWidth= verticalRulerControl.getBounds().width; - ScrollBar horizontalBar= textWidget.getHorizontalBar(); - boolean hScrollVisible= horizontalBar != null && horizontalBar.isVisible(); int rulerHeight= clArea.height - topTrim; if (hScrollVisible) rulerHeight-= scrollbarHeight; @@ -163,16 +163,24 @@ public class SourceViewer extends TextViewer implements ISourceViewer, ISourceVi int[] arrowHeights= getVerticalScrollArrowHeights(textWidget, bottomOffset); int overviewRulerX= clArea.x + clArea.width - overviewRulerWidth - 1; - fOverviewRuler.getControl().setBounds(overviewRulerX, clArea.y + arrowHeights[0], overviewRulerWidth, clArea.height - arrowHeights[0] - arrowHeights[1] - scrollbarHeight); - + boolean noSpaceForHeader= (arrowHeights[0] <= 0 && arrowHeights[1] <= 0 && !hScrollVisible); Control headerControl= fOverviewRuler.getHeaderControl(); - boolean noArrows= arrowHeights[0] < 6 && arrowHeights[1] < 6; // need at least 6px to render the header control - if (noArrows || arrowHeights[0] < arrowHeights[1] && arrowHeights[0] < scrollbarHeight && arrowHeights[1] > scrollbarHeight) { - // // not enough space for header at top => move to bottom - int headerHeight= noArrows ? scrollbarHeight : arrowHeights[1]; - headerControl.setBounds(overviewRulerX, clArea.y + clArea.height - arrowHeights[1] - scrollbarHeight, overviewRulerWidth, headerHeight); + Control rulerControl= fOverviewRuler.getControl(); + if (noSpaceForHeader) { + // If we don't have space to draw because we don't have arrows and the horizontal scroll is invisible, + // use the whole space for the ruler and leave the headerControl without any space (will actually be invisible). + rulerControl.setBounds(overviewRulerX, clArea.y, overviewRulerWidth, clArea.height); + headerControl.setBounds(0, 0, 0, 0); } else { - headerControl.setBounds(overviewRulerX, clArea.y, overviewRulerWidth, arrowHeights[0]); + boolean smallArrows= arrowHeights[0] < 6 && arrowHeights[1] < 6; // need at least 6px to render the header control + rulerControl.setBounds(overviewRulerX, clArea.y + arrowHeights[0], overviewRulerWidth, clArea.height - arrowHeights[0] - arrowHeights[1] - scrollbarHeight); + if (smallArrows || arrowHeights[0] < arrowHeights[1] && arrowHeights[0] < scrollbarHeight && arrowHeights[1] > scrollbarHeight) { + // not enough space for header at top => move to bottom + int headerHeight= smallArrows ? scrollbarHeight : arrowHeights[1]; + headerControl.setBounds(overviewRulerX, clArea.y + clArea.height - arrowHeights[1] - scrollbarHeight, overviewRulerWidth, headerHeight); + } else { + headerControl.setBounds(overviewRulerX, clArea.y, overviewRulerWidth, arrowHeights[0]); + } } headerControl.redraw(); } |