src/Tools/jEdit/src/rich_text_area.scala
changeset 73877 d9ebbfe099a8
parent 73876 e6c9c1c3f580
child 73880 9ce206f6e8c6
equal deleted inserted replaced
73876:e6c9c1c3f580 73877:d9ebbfe099a8
   433         val chunk_text = new AttributedString(chunk_str)
   433         val chunk_text = new AttributedString(chunk_str)
   434 
   434 
   435         def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit =
   435         def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit =
   436           chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset)
   436           chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset)
   437 
   437 
   438 
       
   439         // font
   438         // font
       
   439         chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
   440         chunk_text.addAttribute(TextAttribute.FONT, chunk_font)
   440         chunk_text.addAttribute(TextAttribute.FONT, chunk_font)
   441         chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR)
       
   442         if (chunk.usedFontSubstitution) {
   441         if (chunk.usedFontSubstitution) {
   443           for {
   442           for {
   444             (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c)
   443             (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c)
   445             subst_font = Chunk.getSubstFont(c) if subst_font != null
   444             subst_font = Chunk.getSubstFont(c) if subst_font != null
   446           } {
   445           } {