# 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)