tuned;
authorwenzelm
Mon Jun 13 13:53:41 2011 +0200 (2011-06-13)
changeset 43374df1be524e60c
parent 43373 639c3aca2ed3
child 43375 09d992ab57c6
tuned;
src/Tools/jEdit/src/text_painter.scala
     1.1 --- a/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 12:33:53 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 13:53:41 2011 +0200
     1.3 @@ -81,7 +81,6 @@
     1.4            line_infos.get(start(i)) match {
     1.5              case Some(chunk) =>
     1.6                val w = Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR).toInt
     1.7 -              gfx.setFont(font)
     1.8                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
     1.9                orig_text_painter.paintValidLine(
    1.10                  gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)