use orig_text_painter for extras outside main text (also required to update internal line infos);
authorwenzelm
Mon Jun 13 12:29:26 2011 +0200 (2011-06-13)
changeset 433722df2144b0910
parent 43371 98de43fc9733
child 43373 639c3aca2ed3
use orig_text_painter for extras outside main text (also required to update internal line infos);
tuned;
src/Tools/jEdit/src/text_painter.scala
     1.1 --- a/src/Tools/jEdit/src/text_painter.scala	Sun Jun 12 22:26:03 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 12:29:26 2011 +0200
     1.3 @@ -44,55 +44,52 @@
     1.4          val fm = painter.getFontMetrics
     1.5  
     1.6          // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
     1.7 -        // and org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
     1.8 +        // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
     1.9          val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
    1.10          val soft_wrap = buffer.getStringProperty("wrap") == "soft"
    1.11          val wrap_margin =
    1.12          {
    1.13            val max = buffer.getIntegerProperty("maxLineLen", 0)
    1.14            if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    1.15 -          else if (soft_wrap)
    1.16 -            painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
    1.17 +          else if (soft_wrap) painter.getWidth - char_width * 3
    1.18            else 0
    1.19          }.toFloat
    1.20  
    1.21 -        type Line_Info = (Chunk, Boolean)
    1.22 -        val line_infos: Map[Text.Offset, Line_Info] =
    1.23 +        val line_infos: Map[Text.Offset, Chunk] =
    1.24          {
    1.25 -          import scala.collection.JavaConversions._
    1.26 -
    1.27            val out = new ArrayList[Chunk]
    1.28            val handler = new DisplayTokenHandler
    1.29            val margin = if (soft_wrap) wrap_margin else 0.0f
    1.30  
    1.31 -          var result = Map[Text.Offset, Line_Info]()
    1.32 +          var result = Map[Text.Offset, Chunk]()
    1.33            for (line <- physical_lines.iterator.filter(i => i != -1)) {
    1.34              out.clear
    1.35              handler.init(painter.getStyles, font_context, painter, out, margin)
    1.36              buffer.markTokens(line, handler)
    1.37  
    1.38              val line_start = buffer.getLineStartOffset(line)
    1.39 -            val len = out.size
    1.40 -            for (i <- 0 until len) {
    1.41 +            for (i <- 0 until out.size) {
    1.42                val chunk = out.get(i)
    1.43 -              result += (line_start + chunk.offset -> (chunk, i == len - 1))
    1.44 +              result += (line_start + chunk.offset -> chunk)
    1.45              }
    1.46            }
    1.47            result
    1.48          }
    1.49  
    1.50 +        val clip = gfx.getClip
    1.51          val x0 = text_area.getHorizontalOffset
    1.52          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
    1.53          for (i <- 0 until physical_lines.length) {
    1.54            if (physical_lines(i) != -1) {
    1.55              line_infos.get(start(i)) match {
    1.56 -              case Some((chunk, last_subregion)) =>
    1.57 -                val x1 = x0 + Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
    1.58 -                if (!last_subregion) {
    1.59 -                  gfx.setFont(font)
    1.60 -                  gfx.setColor(painter.getEOLMarkerColor)
    1.61 -                  gfx.drawString(":", (x0 + wrap_margin + char_width) max x1, y0)
    1.62 -                }
    1.63 +              case Some(chunk) =>
    1.64 +                val w = Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR).toInt
    1.65 +                gfx.setFont(font)
    1.66 +                gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
    1.67 +                orig_text_painter.paintValidLine(
    1.68 +                  gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
    1.69 +                gfx.setClip(clip)
    1.70 +
    1.71                case None =>
    1.72              }
    1.73            }