# HG changeset patch
# User wenzelm
# Date 1624714328 -7200
# Node ID 9ce206f6e8c67544e02c4325034bc96f420c37cd
# Parent  0db0cd46216364b788ba428b438cfdfdfda32f0f
tuned;

diff -r 0db0cd462163 -r 9ce206f6e8c6 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Jun 25 22:05:14 2021 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 26 15:32:08 2021 +0200
@@ -489,7 +489,7 @@
         {
           val w = fm.charWidth(' ')
           val b = (w / 2) max 1
-          val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
+          val c = (lm.getAscent + lm.getStrikethroughOffset).round
           ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
         }
 
@@ -505,8 +505,7 @@
               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.toFloat, y0.toFloat).toInt
+                val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0.toFloat, y0.toFloat)
                 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)