diff options
author | skybber | 2016-12-09 16:39:59 +0000 |
---|---|---|
committer | Dani Megert | 2017-05-05 13:55:12 +0000 |
commit | f3f6c3fc71732876a04290b856f7eb62cd52f79b (patch) | |
tree | 445eaac50a0988fd4513185de82e62e1c85c1783 | |
parent | 9402543634c86e5fc7f1652abc12f1c5816ab816 (diff) | |
download | eclipse.platform.text-f3f6c3fc71732876a04290b856f7eb62cd52f79b.tar.gz eclipse.platform.text-f3f6c3fc71732876a04290b856f7eb62cd52f79b.tar.xz eclipse.platform.text-f3f6c3fc71732876a04290b856f7eb62cd52f79b.zip |
Whitespace characters are printed in one block , not separately, if
monospaced font is used.
Change-Id: I2534487ee2b6cf8337be8aea7a900da8f2f44cdb
Signed-off-by: skybber <lada.dvorak7@gmail.com>
-rw-r--r-- | org.eclipse.jface.text/src/org/eclipse/jface/text/WhitespaceCharacterPainter.java | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/org.eclipse.jface.text/src/org/eclipse/jface/text/WhitespaceCharacterPainter.java b/org.eclipse.jface.text/src/org/eclipse/jface/text/WhitespaceCharacterPainter.java index 4a5bd8eeedd..f690aee7ed5 100644 --- a/org.eclipse.jface.text/src/org/eclipse/jface/text/WhitespaceCharacterPainter.java +++ b/org.eclipse.jface.text/src/org/eclipse/jface/text/WhitespaceCharacterPainter.java @@ -215,6 +215,13 @@ public class WhitespaceCharacterPainter implements IPainter, PaintListener { */ private void drawLineRange(GC gc, int startLine, int endLine, int x, int w) { final int viewPortWidth= fTextWidget.getClientArea().width; + int spaceCharWidth = gc.stringExtent(" ").x; //$NON-NLS-1$ + boolean optimizeWhitespacePainting = false; + if ( (spaceCharWidth == gc.stringExtent(String.valueOf(SPACE_SIGN)).x) && + (spaceCharWidth == gc.stringExtent(String.valueOf(IDEOGRAPHIC_SPACE_SIGN)).x)) { + optimizeWhitespacePainting = true; + } + for (int line= startLine; line <= endLine; line++) { int lineOffset= fTextWidget.getOffsetAtLine(line); // line end offset including line delimiter @@ -268,7 +275,7 @@ public class WhitespaceCharacterPainter implements IPainter, PaintListener { } // draw character range if (endOffset > startOffset) { - drawCharRange(gc, startOffset, endOffset, lineOffset, lineEndOffset); + drawCharRange(gc, startOffset, endOffset, lineOffset, lineEndOffset, optimizeWhitespacePainting); } } } @@ -286,7 +293,7 @@ public class WhitespaceCharacterPainter implements IPainter, PaintListener { * @param lineOffset inclusive start index of the line * @param lineEndOffset exclusive end index of the line */ - private void drawCharRange(GC gc, int startOffset, int endOffset, int lineOffset, int lineEndOffset) { + private void drawCharRange(GC gc, int startOffset, int endOffset, int lineOffset, int lineEndOffset, boolean optimizeWhitespacePainting) { StyledTextContent content= fTextWidget.getContent(); String lineText= content.getTextRange(lineOffset, lineEndOffset - lineOffset); int startOffsetInLine= startOffset - lineOffset; @@ -338,8 +345,12 @@ public class WhitespaceCharacterPainter implements IPainter, PaintListener { visibleChar.append(SPACE_SIGN); } } - // 'continue' would improve performance but may produce drawing errors - // for long runs of space if width of space and dot differ + // 'continue' improves performance but may produce drawing errors + // for long runs of space if width of space and dot differ, therefore + // it can be used only for monospace fonts + if (optimizeWhitespacePainting) { + continue; + } break; case '\u3000': // ideographic whitespace if (isEmptyLine) { @@ -359,8 +370,12 @@ public class WhitespaceCharacterPainter implements IPainter, PaintListener { visibleChar.append(IDEOGRAPHIC_SPACE_SIGN); } } - // 'continue' would improve performance but may produce drawing errors - // for long runs of space if width of space and dot differ + // 'continue' improves performance but may produce drawing errors + // for long runs of space if width of space and dot differ, therefore + // it can be used only for monospace fonts + if (optimizeWhitespacePainting) { + continue; + } break; case '\t': if (isEmptyLine) { |