# HG changeset patch
# User wenzelm
# Date 1384800994 -3600
# Node ID 1fd24c96ce9bf381ca12f7efe7a8d77529725bf2
# Parent  865712316b5f98f933a494e7ac37ff9d779ec8ae
caching of blob;
precise file content according to jEdit IO;

diff -r 865712316b5f -r 1fd24c96ce9b src/Tools/jEdit/src/document_model.scala
--- 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
diff -r 865712316b5f -r 1fd24c96ce9b src/Tools/jEdit/src/jedit_thy_load.scala
--- 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()
+  }
 }