# 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.