# HG changeset patch
# User wenzelm
# Date 1305664195 -7200
# Node ID 15727655bee270777e9fdd431993b24d3950a565
# Parent  358769224d94b73760f9a4d370df6ca77145b232
some support for token/chunk handling, imitating jEdit internals;

diff -r 358769224d94 -r 15727655bee2 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue May 17 15:11:36 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue May 17 22:29:55 2011 +0200
@@ -17,12 +17,13 @@
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
 import javax.swing.event.{CaretListener, CaretEvent}
+import java.util.ArrayList
 
 import org.gjt.sp.jedit.{jEdit, OperatingSystem}
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.options.GutterOptionPane
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.SyntaxStyle
+import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token}
 
 
 object Document_View
@@ -67,6 +68,8 @@
   private val session = model.session
 
 
+  /** token handling **/
+
   /* extended token styles */
 
   private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
@@ -85,6 +88,40 @@
   }
 
 
+  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
+
+  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 */
+
+  def line_chunks(physical: Int): java.util.List[Chunk] =
+  {
+    val buffer = text_area.getBuffer
+    val painter = text_area.getPainter
+
+    val handler = new DisplayTokenHandler
+    handler.init(painter.getStyles, painter.getFontRenderContext, painter,
+      new ArrayList[Chunk], wrap_margin().toFloat)
+    buffer.markTokens(physical, handler)
+    handler.getChunkList
+  }
+
+
   /* visible line ranges */
 
   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.