src/Tools/jEdit/src/jedit_thy_load.scala
changeset 54511 1fd24c96ce9b
parent 54509 1f77110c94ef
child 54515 570ba266f5b5
--- 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()
+  }
 }