tuned;
authorwenzelm
Tue Jun 14 13:18:36 2011 +0200 (2011-06-14)
changeset 4338363fc6b5ef8ac
parent 43382 5d9d34bdec25
child 43384 9c228b8953f2
tuned;
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 12:18:34 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 14 13:18:36 2011 +0200
     1.3 @@ -9,12 +9,12 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.awt.{Graphics, Graphics2D}
     1.8 +import java.awt.Graphics2D
     1.9  import java.util.ArrayList
    1.10  
    1.11  import org.gjt.sp.jedit.Debug
    1.12  import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    1.13 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    1.14 +import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
    1.15  
    1.16  
    1.17  class Text_Area_Painter(doc_view: Document_View)
    1.18 @@ -211,12 +211,12 @@
    1.19            gfx.drawGlyphVector(chunk.gv, x + w, y)
    1.20          }
    1.21          else {
    1.22 -          var xpos = x + w
    1.23 +          var x1 = x + w
    1.24            for (Text.Info(range, info) <- markup) {
    1.25              val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.26              gfx.setColor(info.getOrElse(chunk_color))
    1.27 -            gfx.drawString(str, xpos.toInt, y.toInt)
    1.28 -            xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.29 +            gfx.drawString(str, x1.toInt, y.toInt)
    1.30 +            x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
    1.31            }
    1.32          }
    1.33        }