# HG changeset patch
# User wenzelm
# Date 1307903065 -7200
# Node ID 1d6ce56e9b2f46c77a20ba7dfd8b9b968b1f07ef
# Parent  4c86b3405010abcda1bed3d814dab4d0265f1e53
tuned;

diff -r 4c86b3405010 -r 1d6ce56e9b2f src/Tools/jEdit/src/text_painter.scala
--- a/src/Tools/jEdit/src/text_painter.scala	Sun Jun 12 20:08:49 2011 +0200
+++ b/src/Tools/jEdit/src/text_painter.scala	Sun Jun 12 20:24:25 2011 +0200
@@ -29,35 +29,27 @@
     }
   }
 
-
-  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
-
-  private def wrap_margin(): Int =
-  {
-    val buffer = text_area.getBuffer
-    val painter = text_area.getPainter
-    val font = painter.getFont
-    val font_context = painter.getFontRenderContext
-
-    val soft_wrap = buffer.getStringProperty("wrap") == "soft"
-    val max = buffer.getIntegerProperty("maxLineLen", 0)
-
-    if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
-    else if (soft_wrap)
-      painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
-    else 0
-  }
-
-
-  /* chunks */
-
-  private def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
+  def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
   {
     import scala.collection.JavaConversions._
 
     val buffer = text_area.getBuffer
     val painter = text_area.getPainter
-    val margin = wrap_margin().toFloat
+    val wrap_margin =
+      // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
+      // and org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
+    {
+      val font = painter.getFont
+      val font_context = painter.getFontRenderContext
+
+      val soft_wrap = buffer.getStringProperty("wrap") == "soft"
+      val max = buffer.getIntegerProperty("maxLineLen", 0)
+
+      if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
+      else if (soft_wrap)
+        painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
+      else 0
+    }.toFloat
 
     val out = new ArrayList[Chunk]
     val handler = new DisplayTokenHandler
@@ -65,7 +57,7 @@
     var result = Map[Text.Offset, Chunk]()
     for (line <- physical_lines) {
       out.clear
-      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
+      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, wrap_margin)
       buffer.markTokens(line, handler)
 
       val line_start = buffer.getLineStartOffset(line)