src/Tools/jEdit/src/text_area_painter.scala
changeset 44056 be825a69fc67
parent 43759 d93a69672362
child 44545 3c40007aa031
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Aug 08 13:48:38 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Aug 08 16:09:34 2011 +0200
     1.3 @@ -204,6 +204,10 @@
     1.4          val chunk_font = chunk.style.getFont
     1.5          val chunk_color = chunk.style.getForegroundColor
     1.6  
     1.7 +        def string_width(s: String): Float =
     1.8 +          if (s.isEmpty) 0.0f
     1.9 +          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
    1.10 +
    1.11          val caret_range =
    1.12            if (text_area.hasFocus) doc_view.caret_range()
    1.13            else Text.Range(-1)
    1.14 @@ -230,17 +234,27 @@
    1.15  
    1.16            range.try_restrict(caret_range) match {
    1.17              case Some(r) if !r.is_singularity =>
    1.18 -              val astr = new AttributedString(str)
    1.19                val i = r.start - range.start
    1.20                val j = r.stop - range.start
    1.21 +              val s1 = str.substring(0, i)
    1.22 +              val s2 = str.substring(i, j)
    1.23 +              val s3 = str.substring(j)
    1.24 +
    1.25 +              if (!s1.isEmpty) gfx.drawString(s1, x1, y)
    1.26 +
    1.27 +              val astr = new AttributedString(s2)
    1.28                astr.addAttribute(TextAttribute.FONT, chunk_font)
    1.29 -              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
    1.30 -              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
    1.31 -              gfx.drawString(astr.getIterator, x1, y)
    1.32 +              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
    1.33 +              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
    1.34 +              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
    1.35 +
    1.36 +              if (!s3.isEmpty)
    1.37 +                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
    1.38 +
    1.39              case _ =>
    1.40                gfx.drawString(str, x1, y)
    1.41            }
    1.42 -          x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.43 +          x1 += string_width(str)
    1.44          }
    1.45        }
    1.46        w += chunk.width