src/Tools/jEdit/src/rich_text_area.scala

             val chunks = text_area.getChunksOfScreenLine(screen_line)
             if (chunks != null) {
               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)
               } finally { gfx.setClip(clip) }
             }