allow disabling margins around annotations in editor gutter

GitOrigin-RevId: f22952150422600c4084d3ad68ad31df78666de6
This commit is contained in:
Dmitry Batrak
2019-10-03 12:02:50 +00:00
committed by intellij-monorepo-bot
parent cb3cab4569
commit 0c7abbfcd8
2 changed files with 10 additions and 2 deletions
@@ -71,4 +71,12 @@ public interface TextAnnotationGutterProvider {
* @see EditorGutter#closeAllAnnotations()
*/
void gutterClosed();
/**
* If {@code true}, a couple of pixels will be added at both sides of displayed text (if it's not empty),
* otherwise the width of annotation will be equal to the width of provided text.
*/
default boolean useMargin() {
return true;
}
}
@@ -487,7 +487,7 @@ class EditorGutterComponentImpl extends EditorGutterComponentEx implements Mouse
EditorFontType style = gutterProvider.getStyle(line, myEditor);
Font font = getFontForText(s, style);
g.setFont(font);
g.drawString(s, getGapBetweenAnnotations() / 2 + x, y + myEditor.getAscent());
g.drawString(s, (gutterProvider.useMargin() ? getGapBetweenAnnotations() / 2 : 0) + x, y + myEditor.getAscent());
}
}
@@ -772,7 +772,7 @@ class EditorGutterComponentImpl extends EditorGutterComponentEx implements Mouse
gutterSize = Math.max(gutterSize, fontMetrics.stringWidth(lineText));
}
}
if (gutterSize > 0 && j < guttersCount - 1) gutterSize += getGapBetweenAnnotations();
if (gutterSize > 0 && gutterProvider.useMargin()) gutterSize += getGapBetweenAnnotations();
myTextAnnotationGutterSizes.set(j, gutterSize);
myTextAnnotationGuttersSize += gutterSize;
}