--- a/src/Tools/jEdit/src/jedit_thy_load.scala Mon Nov 18 17:24:04 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Mon Nov 18 19:56:34 2013 +0100
@@ -9,13 +9,13 @@
import isabelle._
-import java.io.{File => JFile, IOException}
+import java.io.{File => JFile, IOException, ByteArrayOutputStream}
import javax.swing.text.Segment
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
import org.gjt.sp.jedit.MiscUtilities
import org.gjt.sp.jedit.{View, Buffer}
-
+import org.gjt.sp.jedit.bufferio.BufferIORequest
class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
extends Thy_Load(loaded_theories, base_syntax)
@@ -89,5 +89,28 @@
catch { case _: IOException => }
}
}
+
+
+ /* file content */
+
+ def file_content(buffer: Buffer): Bytes =
+ {
+ val path = buffer.getPath
+ val vfs = VFSManager.getVFSForPath(path)
+ val content =
+ new BufferIORequest(null, buffer, null, vfs, path) {
+ def _run() { }
+ def apply(): Bytes =
+ {
+ val out =
+ new ByteArrayOutputStream(buffer.getLength + 1) {
+ def content(): Bytes = Bytes(this.buf, 0, this.count)
+ }
+ write(buffer, out)
+ out.content()
+ }
+ }
+ content()
+ }
}