src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -131,18 +131,19 @@
 
   /* blob */
 
-  private var _blob: Option[Bytes] = None  // owned by Swing thread
+  private var _blob: Option[(Bytes, Command.File)] = None  // owned by Swing thread
 
   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
 
-  def blob(): Bytes =
+  def blob(): (Bytes, Command.File) =
     Swing_Thread.require {
       _blob match {
-        case Some(b) => b
+        case Some(x) => x
         case None =>
           val b = PIDE.thy_load.file_content(buffer)
-          _blob = Some(b)
-          b
+          val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
+          _blob = Some((b, file))
+          (b, file)
       }
     }