# HG changeset patch
# User wenzelm
# Date 1624716186 -7200
# Node ID 994c9dacd2f963177337f195db62c699cf284d7a
# Parent  01efb7cbf365f9722fb79e7a52155cfc3c9fbb19
more predictable result, avoid slightly odd "lastSubstFont" by jEdit;

diff -r 01efb7cbf365 -r 994c9dacd2f9 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 26 15:52:16 2021 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Jun 26 16:03:06 2021 +0200
@@ -404,6 +404,13 @@
     }
   }
 
+  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,
     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
@@ -413,6 +420,8 @@
       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) {
@@ -441,6 +450,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
           } {
             val r = Text.Range(i, i + Character.charCount(c)) + chunk_offset