diff -r 591598bc52bc -r b6b09fc8d671 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 21:20:22 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 21:26:47 2011 +0200
@@ -213,15 +213,14 @@
 
         val markup =
           for {
-            x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
-            y <- x.try_restrict(chunk_range)
-          } yield y
+            r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
+            r2 <- r1.try_restrict(chunk_range)
+          } yield r2
 
+        var x1 = x + w
         gfx.setFont(chunk_font)
-        if (markup.isEmpty)
-          gfx.drawString(chunk.str, x.toInt, y.toInt)
+        if (markup.isEmpty) gfx.drawString(chunk.str, x1, y)
         else {
-          var x1 = x + w
           for {
             Text.Info(range, info) <-
               Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
@@ -240,9 +239,9 @@
                 astr.addAttribute(TextAttribute.FONT, chunk_font)
                 astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
                 astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
-                gfx.drawString(astr.getIterator, x1.toInt, y.toInt)
+                gfx.drawString(astr.getIterator, x1, y)
               case _ =>
-                gfx.drawString(str, x1.toInt, y.toInt)
+                gfx.drawString(str, x1, y)
             }
             x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
           }