tuned;
authorwenzelm
Sun Jun 12 20:24:25 2011 +0200 (2011-06-12)
changeset 433701d6ce56e9b2f
parent 43369 4c86b3405010
child 43371 98de43fc9733
tuned;
src/Tools/jEdit/src/text_painter.scala
     1.1 --- a/src/Tools/jEdit/src/text_painter.scala	Sun Jun 12 20:08:49 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_painter.scala	Sun Jun 12 20:24:25 2011 +0200
     1.3 @@ -29,35 +29,27 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -
     1.8 -  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
     1.9 -
    1.10 -  private def wrap_margin(): Int =
    1.11 -  {
    1.12 -    val buffer = text_area.getBuffer
    1.13 -    val painter = text_area.getPainter
    1.14 -    val font = painter.getFont
    1.15 -    val font_context = painter.getFontRenderContext
    1.16 -
    1.17 -    val soft_wrap = buffer.getStringProperty("wrap") == "soft"
    1.18 -    val max = buffer.getIntegerProperty("maxLineLen", 0)
    1.19 -
    1.20 -    if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    1.21 -    else if (soft_wrap)
    1.22 -      painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
    1.23 -    else 0
    1.24 -  }
    1.25 -
    1.26 -
    1.27 -  /* chunks */
    1.28 -
    1.29 -  private def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
    1.30 +  def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
    1.31    {
    1.32      import scala.collection.JavaConversions._
    1.33  
    1.34      val buffer = text_area.getBuffer
    1.35      val painter = text_area.getPainter
    1.36 -    val margin = wrap_margin().toFloat
    1.37 +    val wrap_margin =
    1.38 +      // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
    1.39 +      // and org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
    1.40 +    {
    1.41 +      val font = painter.getFont
    1.42 +      val font_context = painter.getFontRenderContext
    1.43 +
    1.44 +      val soft_wrap = buffer.getStringProperty("wrap") == "soft"
    1.45 +      val max = buffer.getIntegerProperty("maxLineLen", 0)
    1.46 +
    1.47 +      if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
    1.48 +      else if (soft_wrap)
    1.49 +        painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
    1.50 +      else 0
    1.51 +    }.toFloat
    1.52  
    1.53      val out = new ArrayList[Chunk]
    1.54      val handler = new DisplayTokenHandler
    1.55 @@ -65,7 +57,7 @@
    1.56      var result = Map[Text.Offset, Chunk]()
    1.57      for (line <- physical_lines) {
    1.58        out.clear
    1.59 -      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
    1.60 +      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, wrap_margin)
    1.61        buffer.markTokens(line, handler)
    1.62  
    1.63        val line_start = buffer.getLineStartOffset(line)