src/Tools/jEdit/src/jedit_resources.scala
changeset 56666 229309cbc508
parent 56502 db2836f65d42
child 56801 8dd9df88f647
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 23 10:49:30 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 23 11:40:42 2014 +0200
     1.3 @@ -85,26 +85,26 @@
     1.4  
     1.5    /* file content */
     1.6  
     1.7 -  def file_content(buffer: Buffer): Bytes =
     1.8 +  private class File_Content_Output(buffer: Buffer) extends
     1.9 +    ByteArrayOutputStream(buffer.getLength + 1)
    1.10 +  {
    1.11 +    def content(): Bytes = Bytes(this.buf, 0, this.count)
    1.12 +  }
    1.13 +
    1.14 +  private class File_Content(buffer: Buffer) extends
    1.15 +    BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath)
    1.16    {
    1.17 -    val path = buffer.getPath
    1.18 -    val vfs = VFSManager.getVFSForPath(path)
    1.19 -    val content =
    1.20 -      new BufferIORequest(null, buffer, null, vfs, path) {
    1.21 -        def _run() { }
    1.22 -        def apply(): Bytes =
    1.23 -        {
    1.24 -          val out =
    1.25 -            new ByteArrayOutputStream(buffer.getLength + 1) {
    1.26 -              def content(): Bytes = Bytes(this.buf, 0, this.count)
    1.27 -            }
    1.28 -          write(buffer, out)
    1.29 -          out.content()
    1.30 -        }
    1.31 -      }
    1.32 -    content()
    1.33 +    def _run() { }
    1.34 +    def content(): Bytes =
    1.35 +    {
    1.36 +      val out = new File_Content_Output(buffer)
    1.37 +      write(buffer, out)
    1.38 +      out.content()
    1.39 +    }
    1.40    }
    1.41  
    1.42 +  def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
    1.43 +
    1.44  
    1.45    /* theory text edits */
    1.46