diff options
author | angelozerr | 2018-03-19 14:37:33 +0000 |
---|---|---|
committer | angelozerr | 2018-03-19 14:37:33 +0000 |
commit | 38559f9b3758759138fe4c90fee9e3d758d70f1b (patch) | |
tree | d5d75ff576ea658256610cdfb1e01bff77e9031b | |
parent | 13d6b5f4f99bd86e86b52c31f3311f4c10e41efa (diff) | |
download | eclipse.platform.text-38559f9b3758759138fe4c90fee9e3d758d70f1b.tar.gz eclipse.platform.text-38559f9b3758759138fe4c90fee9e3d758d70f1b.tar.xz eclipse.platform.text-38559f9b3758759138fe4c90fee9e3d758d70f1b.zip |
Bug 532604 - [CodeMining] Line header content can be drawn on the lineI20180319-2000
text when mining resolve takes time
Change-Id: Ibbecc1be6d7e47ef4a76e9615171adbcee354da3
Signed-off-by: angelozerr <angelo.zerr@gmail.com>
-rw-r--r-- | org.eclipse.jface.text/src/org/eclipse/jface/text/source/inlined/InlinedAnnotationDrawingStrategy.java | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/org.eclipse.jface.text/src/org/eclipse/jface/text/source/inlined/InlinedAnnotationDrawingStrategy.java b/org.eclipse.jface.text/src/org/eclipse/jface/text/source/inlined/InlinedAnnotationDrawingStrategy.java index 46268a1f809..adaa340de8f 100644 --- a/org.eclipse.jface.text/src/org/eclipse/jface/text/source/inlined/InlinedAnnotationDrawingStrategy.java +++ b/org.eclipse.jface.text/src/org/eclipse/jface/text/source/inlined/InlinedAnnotationDrawingStrategy.java @@ -162,12 +162,16 @@ class InlinedAnnotationDrawingStrategy implements IDrawingStrategy { * @return the style to apply with GlyphMetrics ascent only if needed. */ static StyleRange updateStyle(LineHeaderAnnotation annotation, StyleRange style) { + int width= annotation.getRedrawnCharacterWidth(); + if (width == 0) { + // Update GlyphMetrics only when mining was already drawn + return null; + } int height= annotation.getHeight(); if (height == 0) { return null; } int fullHeight= height + annotation.getRedrawnCharacterHeight(); - int width= annotation.getRedrawnCharacterWidth(); if (style == null) { style= new StyleRange(); Position position= annotation.getPosition(); |