src/Tools/jEdit/src/text_area_painter.scala
changeset 43450 b6b09fc8d671
parent 43448 90aec5043461
child 43451 be760a642d38
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 21:20:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 21:26:47 2011 +0200
     1.3 @@ -213,15 +213,14 @@
     1.4  
     1.5          val markup =
     1.6            for {
     1.7 -            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
     1.8 -            y <- x.try_restrict(chunk_range)
     1.9 -          } yield y
    1.10 +            r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
    1.11 +            r2 <- r1.try_restrict(chunk_range)
    1.12 +          } yield r2
    1.13  
    1.14 +        var x1 = x + w
    1.15          gfx.setFont(chunk_font)
    1.16 -        if (markup.isEmpty)
    1.17 -          gfx.drawString(chunk.str, x.toInt, y.toInt)
    1.18 +        if (markup.isEmpty) gfx.drawString(chunk.str, x1, y)
    1.19          else {
    1.20 -          var x1 = x + w
    1.21            for {
    1.22              Text.Info(range, info) <-
    1.23                Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
    1.24 @@ -240,9 +239,9 @@
    1.25                  astr.addAttribute(TextAttribute.FONT, chunk_font)
    1.26                  astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
    1.27                  astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
    1.28 -                gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
    1.29 +                gfx.drawString(astr.getIterator, x1, y)
    1.30                case _ =>
    1.31 -                gfx.drawString(str, x1.toInt, y.toInt)
    1.32 +                gfx.drawString(str, x1, y)
    1.33              }
    1.34              x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.35            }