diff options
Diffstat (limited to 'org.eclipse.ui.workbench.texteditor/src/org/eclipse/ui/internal/views/minimap/MinimapWidget.java')
-rw-r--r-- | org.eclipse.ui.workbench.texteditor/src/org/eclipse/ui/internal/views/minimap/MinimapWidget.java | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/org.eclipse.ui.workbench.texteditor/src/org/eclipse/ui/internal/views/minimap/MinimapWidget.java b/org.eclipse.ui.workbench.texteditor/src/org/eclipse/ui/internal/views/minimap/MinimapWidget.java index 2fd40a493a4..8df7e1955ff 100644 --- a/org.eclipse.ui.workbench.texteditor/src/org/eclipse/ui/internal/views/minimap/MinimapWidget.java +++ b/org.eclipse.ui.workbench.texteditor/src/org/eclipse/ui/internal/views/minimap/MinimapWidget.java @@ -191,7 +191,7 @@ public class MinimapWidget { FontData fontDatum = fontData[0]; scaledFont = new Font(editorFont.getDevice(), fontDatum.getName(), - Math.round(fontDatum.getHeight() * getScale()), fontDatum.getStyle()); + (int) Math.ceil(fontDatum.getHeight() * getScale()), fontDatum.getStyle()); fScaledFonts.put(editorFont, scaledFont); return scaledFont; } @@ -209,7 +209,11 @@ public class MinimapWidget { @Override public void viewportChanged(int verticalOffset) { - updateMinimap(); + fMinimapTextWidget.getDisplay().asyncExec(() -> { + if (!fMinimapTextWidget.isDisposed()) { + updateMinimap(); + } + }); } void updateMinimap() { |