--- a/src/Tools/jEdit/src/document_model.scala Mon Nov 18 17:24:04 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Nov 18 19:56:34 2013 +0100
@@ -116,10 +116,20 @@
/* blob */
- // FIXME caching
- // FIXME precise file content (encoding)
+ private var _blob: Option[Bytes] = None // owned by Swing thread
+
+ private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
+
def blob(): Bytes =
- Swing_Thread.require { Bytes(buffer.getText(0, buffer.getLength)) }
+ Swing_Thread.require {
+ _blob match {
+ case Some(b) => b
+ case None =>
+ val b = PIDE.thy_load.file_content(buffer)
+ _blob = Some(b)
+ b
+ }
+ }
/* edits */
@@ -191,6 +201,8 @@
def edit(clear: Boolean, e: Text.Edit)
{
+ reset_blob()
+
if (clear) {
pending_clear = true
pending.clear
--- 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()
+ }
}