# HG changeset patch
# User wenzelm
# Date 1720733814 -7200
# Node ID 69e21910febcea524929be57240dd6e3244490e5
# Parent  08034bb75ee8956f0eabba176f002b6dd22537e5
clarified signature: afford explicit Scala data types;

diff -r 08034bb75ee8 -r 69e21910febc src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Jul 11 22:39:04 2024 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Jul 11 23:36:54 2024 +0200
@@ -18,10 +18,11 @@
 import java.text.AttributedString
 
 import scala.util.matching.Regex
+import scala.collection.mutable
 
 import org.gjt.sp.util.Log
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.syntax.{Chunk => JEditChunk}
+import org.gjt.sp.jedit.syntax.{Chunk => JEditChunk, SyntaxStyle}
 import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
 
 
@@ -419,13 +420,40 @@
         })
   }
 
+  sealed case class Chunk(
+    id: Byte,
+    style: SyntaxStyle,
+    offset: Int,
+    length: Int,
+    width: Float,
+    font_subst: Boolean,
+    str: String
+  )
+
+  private def make_chunk_list(chunk_head: JEditChunk): List[Chunk] = {
+    val buf = new mutable.ListBuffer[Chunk]
+    var chunk = chunk_head
+    while (chunk != null) {
+      val str =
+        if (chunk.chars == null) Symbol.spaces(chunk.length)
+        else {
+          if (chunk.str == null) { chunk.str = new String(chunk.chars) }
+          chunk.str
+        }
+      buf += Chunk(chunk.id, chunk.style, chunk.offset, chunk.length, chunk.width,
+        chunk.usedFontSubstitution, str)
+      chunk = chunk.next.asInstanceOf[JEditChunk]
+    }
+    buf.toList
+  }
+
   private def paint_chunk_list(
     rendering: JEdit_Rendering,
     font_subst: Font_Subst,
     gfx: Graphics2D,
     line_start: Text.Offset,
     caret_range: Text.Range,
-    chunk_list: JEditChunk,
+    chunk_list: List[Chunk],
     x0: Int,
     y0: Int
   ): Float = {
@@ -433,23 +461,14 @@
 
     val x = x0.toFloat
     val y = y0.toFloat
-    var w = 0.0f
-    var chunk = chunk_list
-    while (chunk != null) {
+    chunk_list.foldLeft(0.0f) { case (w, chunk) =>
       val chunk_offset = line_start + chunk.offset
       if (x + w + chunk.width > clip_rect.x &&
           x + w < clip_rect.x + clip_rect.width && chunk.length > 0) {
         val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
-        val chunk_str =
-          if (chunk.chars == null) Symbol.spaces(chunk.length)
-          else {
-            if (chunk.str == null) { chunk.str = new String(chunk.chars) }
-            chunk.str
-          }
         val chunk_font = chunk.style.getFont
         val chunk_color = chunk.style.getForegroundColor
-
-        val chunk_text = new AttributedString(chunk_str)
+        val chunk_text = new AttributedString(chunk.str)
 
         def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit =
           chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset)
@@ -457,9 +476,9 @@
         // font
         chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
         chunk_text.addAttribute(TextAttribute.FONT, chunk_font)
-        if (chunk.usedFontSubstitution) {
+        if (chunk.font_subst) {
           for {
-            (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c)
+            (c, i) <- Codepoint.iterator_offset(chunk.str) if !chunk_font.canDisplay(c)
             subst_font <- font_subst.get(c)
           } {
             val r = Text.Range(i, i + Character.charCount(c)) + chunk_offset
@@ -483,10 +502,8 @@
 
         gfx.drawString(chunk_text.getIterator, x + w, y)
       }
-      w += chunk.width
-      chunk = chunk.next.asInstanceOf[JEditChunk]
+      w + chunk.width
     }
-    w
   }
 
   private val text_painter = new TextAreaExtension {
@@ -525,8 +542,8 @@
 
             // text chunks
             val screen_line = first_line + i
-            val chunks = text_area.getChunksOfScreenLine(screen_line)
-            if (chunks != null) {
+            val chunk_list = make_chunk_list(text_area.getChunksOfScreenLine(screen_line))
+            if (chunk_list.nonEmpty) {
               try {
                 val line_start = buffer.getLineStartOffset(line)
                 val caret_range =
@@ -535,7 +552,7 @@
                 gfx.clipRect(x0, y + line_height * i, Int.MaxValue, line_height)
                 val w =
                   paint_chunk_list(rendering, font_subst, gfx,
-                    line_start, caret_range, chunks, x0, y0)
+                    line_start, caret_range, chunk_list, x0, y0)
                 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)