# 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