# HG changeset patch
# User wenzelm
# Date 1624648497 -7200
# Node ID e6c9c1c3f580705aea0f8818583ff252132bf1e8
# Parent  6e43936f2111d77e37a7fc26a8249740b6b5d72d
support for jEdit font substitution;

diff -r 6e43936f2111 -r e6c9c1c3f580 NEWS
--- a/NEWS	Fri Jun 25 20:30:14 2021 +0200
+++ b/NEWS	Fri Jun 25 21:14:57 2021 +0200
@@ -31,6 +31,8 @@
 
 * More robust 'proof' outline for method "induct": support nested cases.
 
+* Support for built-in font substitution of jEdit text area.
+
 
 *** Document preparation ***
 
diff -r 6e43936f2111 -r e6c9c1c3f580 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Jun 25 20:30:14 2021 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Jun 25 21:14:57 2021 +0200
@@ -439,6 +439,16 @@
         // font
         chunk_text.addAttribute(TextAttribute.FONT, chunk_font)
         chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
+        if (chunk.usedFontSubstitution) {
+          for {
+            (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c)
+            subst_font = Chunk.getSubstFont(c) if subst_font != null
+          } {
+            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)
+          }
+        }
 
         // color
         chunk_text.addAttribute(TextAttribute.FOREGROUND, chunk_color)