--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Jun 25 21:14:57 2021 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Jun 25 21:16:53 2021 +0200
@@ -435,10 +435,9 @@
def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit =
chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset)
-
// font
+ chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
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)