# HG changeset patch
# User wenzelm
# Date 1720730344 -7200
# Node ID 08034bb75ee8956f0eabba176f002b6dd22537e5
# Parent  6be239aa5cdbb4c188bc203389f929675d39913b
tuned signature;

diff -r 6be239aa5cdb -r 08034bb75ee8 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Jul 11 22:29:54 2024 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Jul 11 22:39:04 2024 +0200
@@ -21,7 +21,7 @@
 
 import org.gjt.sp.util.Log
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.syntax.Chunk
+import org.gjt.sp.jedit.syntax.{Chunk => JEditChunk}
 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
 
 
@@ -410,10 +410,10 @@
     def get(codepoint: Int): Option[Font] =
       cache.getOrElse(codepoint,
         {
-          val field = classOf[Chunk].getDeclaredField("lastSubstFont")
+          val field = classOf[JEditChunk].getDeclaredField("lastSubstFont")
           field.setAccessible(true)
           field.set(null, null)
-          val res = Option(Chunk.getSubstFont(codepoint))
+          val res = Option(JEditChunk.getSubstFont(codepoint))
           cache += (codepoint -> res)
           res
         })
@@ -425,7 +425,7 @@
     gfx: Graphics2D,
     line_start: Text.Offset,
     caret_range: Text.Range,
-    head: Chunk,
+    chunk_list: JEditChunk,
     x0: Int,
     y0: Int
   ): Float = {
@@ -434,7 +434,7 @@
     val x = x0.toFloat
     val y = y0.toFloat
     var w = 0.0f
-    var chunk = head
+    var chunk = chunk_list
     while (chunk != null) {
       val chunk_offset = line_start + chunk.offset
       if (x + w + chunk.width > clip_rect.x &&
@@ -463,7 +463,7 @@
             subst_font <- font_subst.get(c)
           } {
             val r = Text.Range(i, i + Character.charCount(c)) + chunk_offset
-            val font = Chunk.deriveSubstFont(chunk_font, subst_font)
+            val font = JEditChunk.deriveSubstFont(chunk_font, subst_font)
             chunk_attrib(TextAttribute.FONT, font, r)
           }
         }
@@ -484,7 +484,7 @@
         gfx.drawString(chunk_text.getIterator, x + w, y)
       }
       w += chunk.width
-      chunk = chunk.next.asInstanceOf[Chunk]
+      chunk = chunk.next.asInstanceOf[JEditChunk]
     }
     w
   }