# HG changeset patch
# User wenzelm
# Date 1308050316 -7200
# Node ID 63fc6b5ef8ac7a44f5e33c83facf7628ef5cfded
# Parent  5d9d34bdec256351217b5c09ef8b872038d1ccee
tuned;

diff -r 5d9d34bdec25 -r 63fc6b5ef8ac src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 12:18:34 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 13:18:36 2011 +0200
@@ -9,12 +9,12 @@
 
 import isabelle._
 
-import java.awt.{Graphics, Graphics2D}
+import java.awt.Graphics2D
 import java.util.ArrayList
 
 import org.gjt.sp.jedit.Debug
 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
 
 
 class Text_Area_Painter(doc_view: Document_View)
@@ -211,12 +211,12 @@
           gfx.drawGlyphVector(chunk.gv, x + w, y)
         }
         else {
-          var xpos = x + w
+          var x1 = x + w
           for (Text.Info(range, info) <- markup) {
             val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
             gfx.setColor(info.getOrElse(chunk_color))
-            gfx.drawString(str, xpos.toInt, y.toInt)
-            xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+            gfx.drawString(str, x1.toInt, y.toInt)
+            x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
           }
         }
       }