src/Tools/jEdit/src/rich_text_area.scala

 package isabelle.jedit
 
 
 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
 import javax.swing.SwingUtilities
 import java.text.AttributedString

         rendering.caret_debugger_color
       else rendering.caret_invisible_color
     }
   }
 
-  private def reset_subst_font(): Unit =
-  {
-    val field = classOf[Chunk].getDeclaredField("lastSubstFont")
-    field.setAccessible(true)
-    field.set(null, null)
-  }
-
-  private def paint_chunk_list(rendering: JEdit_Rendering,
+  private class Font_Subst
+  {
+    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, font_subst: Font_Subst,
     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
     val clip_rect = gfx.getClipBounds
 
     val caret_range =
       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) {
       val chunk_offset = line_start + chunk.offset

         chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
         chunk_text.addAttribute(TextAttribute.FONT, chunk_font)
         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)
             chunk_attrib(TextAttribute.FONT, font, r)
           }

           val w = fm.charWidth(' ')
           val b = (w / 2) max 1
           val c = (lm.getAscent + lm.getStrikethroughOffset).round
           ((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) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)

             val chunks = text_area.getChunksOfScreenLine(screen_line)
             if (chunks != null) {
               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)
               } finally { gfx.setClip(clip) }
             }