# HG changeset patch
# User wenzelm
# Date 1720729794 -7200
# Node ID 6be239aa5cdbb4c188bc203389f929675d39913b
# Parent  a66a962b015bd849aec0a6426c0729c04494af28
tuned signature (again);

diff -r a66a962b015b -r 6be239aa5cdb src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Jul 11 18:25:25 2024 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Jul 11 22:29:54 2024 +0200
@@ -428,7 +428,7 @@
     head: Chunk,
     x0: Int,
     y0: Int
-  ): Int = {
+  ): Float = {
     val clip_rect = gfx.getClipBounds
 
     val x = x0.toFloat
@@ -486,7 +486,7 @@
       w += chunk.width
       chunk = chunk.next.asInstanceOf[Chunk]
     }
-    w.toInt
+    w
   }
 
   private val text_painter = new TextAreaExtension {
@@ -536,7 +536,7 @@
                 val w =
                   paint_chunk_list(rendering, font_subst, gfx,
                     line_start, caret_range, chunks, x0, y0)
-                gfx.clipRect(x0 + w, 0, Int.MaxValue, Int.MaxValue)
+                gfx.clipRect(x0 + w.toInt, 0, Int.MaxValue, Int.MaxValue)
                 orig_text_painter.paintValidLine(gfx,
                   screen_line, line, start(i), end(i), y + line_height * i)
               } finally { gfx.setClip(clip) }