# HG changeset patch
# User wenzelm
# Date 1624733743 -7200
# Node ID 0a12ca4f3e8d5345f6c96803ef828aa364076bbf
# Parent  994c9dacd2f963177337f195db62c699cf284d7a
proper Font_Subst.cache for paintScreenLineRange;

diff -r 994c9dacd2f9 -r 0a12ca4f3e8d src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 26 16:03:06 2021 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 26 20:55:43 2021 +0200
@@ -10,7 +10,7 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo}
+import java.awt.{Graphics2D, Shape, Color, Point, Cursor, MouseInfo, Font}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, KeyEvent}
 import java.awt.font.TextAttribute
@@ -404,14 +404,23 @@
     }
   }
 
-  private def reset_subst_font(): Unit =
+  private class Font_Subst
   {
-    val field = classOf[Chunk].getDeclaredField("lastSubstFont")
-    field.setAccessible(true)
-    field.set(null, null)
+    private var cache = Map.empty[Int, Option[Font]]
+
+    def get(codepoint: Int): Option[Font] =
+      cache.getOrElse(codepoint,
+        {
+          val field = classOf[Chunk].getDeclaredField("lastSubstFont")
+          field.setAccessible(true)
+          field.set(null, null)
+          val res = Option(Chunk.getSubstFont(codepoint))
+          cache += (codepoint -> res)
+          res
+        })
   }
 
-  private def paint_chunk_list(rendering: JEdit_Rendering,
+  private def paint_chunk_list(rendering: JEdit_Rendering, font_subst: Font_Subst,
     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
     val clip_rect = gfx.getClipBounds
@@ -420,8 +429,6 @@
       if (caret_enabled) JEdit_Lib.caret_range(text_area)
       else Text.Range.offside
 
-    reset_subst_font()
-
     var w = 0.0f
     var chunk = head
     while (chunk != null) {
@@ -450,8 +457,7 @@
         if (chunk.usedFontSubstitution) {
           for {
             (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c)
-            _ = reset_subst_font()
-            subst_font = Chunk.getSubstFont(c) if subst_font != null
+            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)
@@ -503,6 +509,8 @@
           ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
         }
 
+        val font_subst = new Font_Subst
+
         for (i <- physical_lines.indices) {
           val line = physical_lines(i)
           if (line != -1) {
@@ -515,7 +523,9 @@
               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)
+                val w =
+                  paint_chunk_list(rendering, font_subst, 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)