src/Tools/jEdit/src/jedit_resources.scala
changeset 56823 37be55461dbe
parent 56801 8dd9df88f647
child 57612 990ffb84489b
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Fri May 02 12:27:40 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri May 02 13:52:45 2014 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4  import java.io.{File => JFile, ByteArrayOutputStream}
     1.5  import javax.swing.text.Segment
     1.6  
     1.7 +import scala.util.parsing.input.Reader
     1.8 +
     1.9  import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    1.10  import org.gjt.sp.jedit.MiscUtilities
    1.11  import org.gjt.sp.jedit.{jEdit, View, Buffer}
    1.12 @@ -58,21 +60,19 @@
    1.13      }
    1.14    }
    1.15  
    1.16 -  override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
    1.17 +  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.18    {
    1.19      Swing_Thread.now {
    1.20        JEdit_Lib.jedit_buffer(name) match {
    1.21          case Some(buffer) =>
    1.22 -          JEdit_Lib.buffer_lock(buffer) {
    1.23 -            Some(consume(buffer.getSegment(0, buffer.getLength)))
    1.24 -          }
    1.25 +          JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
    1.26          case None => None
    1.27        }
    1.28      } getOrElse {
    1.29 -      if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
    1.30 +      if (Url.is_wellformed(name.node)) f(Scan.byte_reader(Url(name.node)))
    1.31        else {
    1.32          val file = new JFile(name.node)
    1.33 -        if (file.isFile) consume(File.read(file))
    1.34 +        if (file.isFile) f(Scan.byte_reader(file))
    1.35          else error("No such file: " + quote(file.toString))
    1.36        }
    1.37      }