src/Tools/jEdit/src/jedit_lib.scala
changeset 56823 37be55461dbe
parent 56774 2d39c313f39e
child 56930 42b5d216dc8c
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri May 02 12:27:40 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri May 02 13:52:45 2014 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
     1.5  
     1.6  import scala.annotation.tailrec
     1.7 +import scala.util.parsing.input.CharSequenceReader
     1.8  
     1.9  import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
    1.10  import org.gjt.sp.jedit.gui.KeyEventWorkaround
    1.11 @@ -97,6 +98,9 @@
    1.12    def buffer_text(buffer: JEditBuffer): String =
    1.13      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    1.14  
    1.15 +  def buffer_reader(buffer: JEditBuffer): CharSequenceReader =
    1.16 +    new CharSequenceReader(buffer.getSegment(0, buffer.getLength))
    1.17 +
    1.18    def buffer_mode(buffer: JEditBuffer): String =
    1.19    {
    1.20      val mode = buffer.getMode