Keep the height reserved by a code mining in sync with the font

bundles/org.eclipse.jface.text/src/org/eclipse/jface/text/source/inlined/InlinedAnnotationSupport.java

@@ -31,6 +31,7 @@
 import org.eclipse.swt.events.MouseEvent;
 import org.eclipse.swt.events.MouseListener;
 import org.eclipse.swt.events.MouseMoveListener;
+import org.eclipse.swt.events.PaintListener;
 import org.eclipse.swt.graphics.Color;
 import org.eclipse.swt.graphics.Device;
 import org.eclipse.swt.graphics.Font;
@@ -43,6 +44,7 @@
 import org.eclipse.core.runtime.Assert;
 
 import org.eclipse.jface.internal.text.codemining.CodeMiningLineContentAnnotation;
+import org.eclipse.jface.internal.text.codemining.CodeMiningLineHeaderAnnotation;
 
 import org.eclipse.jface.text.BadLocationException;
 import org.eclipse.jface.text.DocumentEvent;
@@ -343,6 +345,19 @@ public void mouseUp(MouseEvent e) {
 
 	private FontMetrics fFontMetrics;
 
+	/**
+	 * The line height the reserved heights of the line header annotations were computed
+	 * with, {@code 0} when none were computed yet.
+	 */
+	private int fReservedHeightsLineHeight;
+
+	private boolean fReservedHeightsRefreshPending;
+
+	/**
+	 * Notices a changed line height of the text widget, as SWT reports none.
+	 */
+	private PaintListener fLineHeightTracker;
+
 	/**
 	 * Install the inlined annotation support for the given viewer.
 	 *
@@ -376,6 +391,70 @@ public void install(ISourceViewer viewer, AnnotationPainter painter) {
 		gc.setFont(viewer.getTextWidget().getFont());
 		fFontMetrics= gc.getFontMetrics();
 		gc.dispose();
+		fReservedHeightsLineHeight= lineHeight(text);
+		fLineHeightTracker= e -> refreshReservedHeightsOnLineHeightChange();
+		text.addPaintListener(fLineHeightTracker);
+	}
+
+	/**
+	 * The height a line header annotation reserves per line of its label.
+	 */
+	private static int lineHeight(StyledText text) {
+		return text.getLineHeight() + text.getLineSpacing();
+	}
+
+	/**
+	 * A line header annotation reserves its vertical space while it is painted, so an
+	 * annotation that is out of view keeps the space of the font it was last painted
+	 * with. That leaves the lines below it misplaced until they are scrolled into
+	 * view, which is why the reserved heights are refreshed here. SWT reports no font
+	 * change, so the redraw such a change triggers is what this notices.
+	 */
+	private void refreshReservedHeightsOnLineHeightChange() {
+		StyledText text= fViewer != null ? fViewer.getTextWidget() : null;
+		if (text == null || text.isDisposed() || fReservedHeightsRefreshPending
+				|| lineHeight(text) == fReservedHeightsLineHeight) {
+			return;
+		}
+		fReservedHeightsRefreshPending= true;
+		// the widget is painting itself with the new line height right now, so wait
+		text.getDisplay().asyncExec(() -> {
+			fReservedHeightsRefreshPending= false;
+			if (!text.isDisposed()) {
+				refreshReservedHeights(text);
+			}
+		});
+	}
+
+	private void refreshReservedHeights(StyledText text) {
+		fReservedHeightsLineHeight= lineHeight(text);
+		Set<AbstractInlinedAnnotation> annotations= fInlinedAnnotations;
+		if (annotations == null) {
+			return;
+		}
+		GC gc= new GC(text);
+		try {
+			for (AbstractInlinedAnnotation annotation : annotations) {
+				if (!(annotation instanceof LineHeaderAnnotation header) || annotation.isMarkedDeleted()) {
+					continue;
+				}
+				// only the lines that already reserve space, the others reserve it as
+				// soon as they are painted
+				int line= header.oldLine;
+				if (line < 0 || line >= text.getLineCount() || text.getLineVerticalIndent(line) <= 0) {
+					continue;
+				}
+				int height= header instanceof CodeMiningLineHeaderAnnotation mining ? mining.getHeight(gc)
+						: header.getHeight();
+				// a height of zero is left to the painting, which can tell an annotation
+				// that lost its content from one that is not resolved yet
+				if (height > 0) {
+					text.setLineVerticalIndent(line, height);
+				}
+			}
+		} finally {
+			gc.dispose();
+		}
 	}
 
 	/**
@@ -403,7 +482,12 @@ public void uninstall() {
 		if (text != null && !text.isDisposed()) {
 			text.removeMouseListener(this.fMouseTracker);
 			text.removeMouseMoveListener(this.fMouseTracker);
+			if (fLineHeightTracker != null) {
+				text.removePaintListener(fLineHeightTracker);
+			}
 		}
+		fLineHeightTracker= null;
+		fReservedHeightsLineHeight= 0;
 		if (fViewer != null) {
 			if (fViewer instanceof ITextViewerExtension4) {
 				((ITextViewerExtension4) fViewer).removeTextPresentationListener(updateStylesWidth);

tests/org.eclipse.jface.text.tests/src/org/eclipse/jface/text/tests/codemining/CodeMiningTest.java

@@ -36,6 +36,8 @@
 import org.eclipse.swt.SWT;
 import org.eclipse.swt.custom.StyleRange;
 import org.eclipse.swt.custom.StyledText;
+import org.eclipse.swt.graphics.Font;
+import org.eclipse.swt.graphics.FontData;
 import org.eclipse.swt.graphics.GC;
 import org.eclipse.swt.graphics.Image;
 import org.eclipse.swt.graphics.ImageData;
@@ -750,6 +752,63 @@ List<ICodeMining> createCodeMiningsFor(IDocument document) {
 		}
 	}
 
+	/**
+	 * A line header annotation reserves its vertical space while it is painted, so
+	 * the lines that are out of view when the font changes must not be left with the
+	 * space of the old font.
+	 */
+	@Test
+	public void testReservedHeightFollowsAFontChange() {
+		StringBuilder text= new StringBuilder();
+		for (int i= 0; i < 200; i++) {
+			text.append("line ").append(i).append('\n');
+		}
+		fViewer.getDocument().set(text.toString());
+		StyledText widget= fViewer.getTextWidget();
+		// let a line far below the view port reserve its space, then scroll back to
+		// the top so that it is out of view when the font changes
+		widget.setTopIndex(150);
+		Assertions.assertTrue(new DisplayHelper() {
+			@Override
+			protected boolean condition() {
+				return widget.getLineVerticalIndent(151) > 0;
+			}
+		}.waitForCondition(widget.getDisplay(), 3000), "no code mining below the view port");
+		widget.setTopIndex(0);
+		Assertions.assertTrue(new DisplayHelper() {
+			@Override
+			protected boolean condition() {
+				return widget.getLineVerticalIndent(0) > 0;
+			}
+		}.waitForCondition(widget.getDisplay(), 3000), "no code mining was rendered");
+
+		FontData[] enlarged= widget.getFont().getFontData();
+		for (FontData data : enlarged) {
+			data.setHeight(data.getHeight() * 2);
+		}
+		Font biggerFont= new Font(widget.getDisplay(), enlarged);
+		try {
+			widget.setFont(biggerFont);
+			// a settle time rather than a condition: waiting for a single line to take
+			// the new size lets the ones out of view keep the old one unnoticed
+			DisplayHelper.sleep(widget.getDisplay(), 500);
+
+			int reserving= 0;
+			for (int line= 0; line < widget.getLineCount(); line++) {
+				int reserved= widget.getLineVerticalIndent(line);
+				if (reserved > 0) {
+					reserving++;
+					Assertions.assertEquals(widget.getLineHeight(), reserved,
+							"line " + line + " still reserves the space of the previous font");
+				}
+			}
+			Assertions.assertTrue(reserving > 0, "no line reserved space for a code mining");
+		} finally {
+			widget.setFont(null);
+			biggerFont.dispose();
+		}
+	}
+
 	private static class ReferenceInLineCodeMining extends LineContentCodeMining {
 
 		public ReferenceInLineCodeMining(String label, int positionOffset, ICodeMiningProvider provider) {