src/Tools/jEdit/src/text_area_painter.scala

           if (text_area.hasFocus) doc_view.caret_range()
           else Text.Range(-1)
 
         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)) ++
               markup.iterator ++
               Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))

                 val i = r.start - range.start
                 val j = r.stop - range.start
                 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
           }
         }
       }