diff -r 0bf768567d9f -r d0378baf7d06 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 01 22:37:33 2021 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 01 22:50:00 2021 +0100
@@ -523,7 +523,8 @@
               try {
                 val line_start = buffer.getLineStartOffset(line)
                 gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
-                val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
+                val w =
+                  paint_chunk_list(rendering, gfx, line_start, chunks, x0.toFloat, y0.toFloat).toInt
                 gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
                 orig_text_painter.paintValidLine(gfx,
                   screen_line, line, start(i), end(i), y + line_height * i)