more uniform padded_markup, which is important for caret visibility despite absence of markup;
authorwenzelm
Mon Jul 11 22:19:11 2011 +0200 (2011-07-11)
changeset 43759d93a69672362
parent 43758 52310132063b
child 43760 ef8375a4dae4
more uniform padded_markup, which is important for caret visibility despite absence of markup;
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Jul 11 17:22:31 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Jul 11 22:19:11 2011 +0200
     1.3 @@ -214,37 +214,33 @@
     1.4              r2 <- r1.try_restrict(chunk_range)
     1.5            } yield r2
     1.6  
     1.7 +        val padded_markup =
     1.8 +          if (markup.isEmpty)
     1.9 +            Iterator(Text.Info(chunk_range, None))
    1.10 +          else
    1.11 +            Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
    1.12 +            markup.iterator ++
    1.13 +            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
    1.14 +
    1.15          var x1 = x + w
    1.16          gfx.setFont(chunk_font)
    1.17 -        if (markup.isEmpty) {
    1.18 -          gfx.setColor(chunk_color)
    1.19 -          gfx.drawString(chunk.str, x1, y)
    1.20 -        }
    1.21 -        else {
    1.22 -          for {
    1.23 -            Text.Info(range, info) <-
    1.24 -              Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
    1.25 -              markup.iterator ++
    1.26 -              Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
    1.27 -            if !range.is_singularity
    1.28 -          } {
    1.29 -            val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.30 -            gfx.setColor(info.getOrElse(chunk_color))
    1.31 +        for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
    1.32 +          val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.33 +          gfx.setColor(info.getOrElse(chunk_color))
    1.34  
    1.35 -            range.try_restrict(caret_range) match {
    1.36 -              case Some(r) if !r.is_singularity =>
    1.37 -                val astr = new AttributedString(str)
    1.38 -                val i = r.start - range.start
    1.39 -                val j = r.stop - range.start
    1.40 -                astr.addAttribute(TextAttribute.FONT, chunk_font)
    1.41 -                astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
    1.42 -                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
    1.43 -                gfx.drawString(astr.getIterator, x1, y)
    1.44 -              case _ =>
    1.45 -                gfx.drawString(str, x1, y)
    1.46 -            }
    1.47 -            x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.48 +          range.try_restrict(caret_range) match {
    1.49 +            case Some(r) if !r.is_singularity =>
    1.50 +              val astr = new AttributedString(str)
    1.51 +              val i = r.start - range.start
    1.52 +              val j = r.stop - range.start
    1.53 +              astr.addAttribute(TextAttribute.FONT, chunk_font)
    1.54 +              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
    1.55 +              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
    1.56 +              gfx.drawString(astr.getIterator, x1, y)
    1.57 +            case _ =>
    1.58 +              gfx.drawString(str, x1, y)
    1.59            }
    1.60 +          x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.61          }
    1.62        }
    1.63        w += chunk.width