# HG changeset patch
# User wenzelm
# Date 1393506923 -3600
# Node ID 9b243afbbe8393ebb4a22c282198017796172973
# Parent  da0513d951556ae4aebc2b9fc10beda47c6bf47c
proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;

diff -r da0513d95155 -r 9b243afbbe83 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 14:07:04 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Feb 27 14:15:23 2014 +0100
@@ -164,13 +164,13 @@
 
   /* edits */
 
-  def init_edits(): List[Document.Edit_Text] =
+  def init_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
   {
     Swing_Thread.require()
 
     val header = node_header()
     val text = JEdit_Lib.buffer_text(buffer)
-    val (_, perspective) = node_perspective(Document.Blobs.empty)
+    val (_, perspective) = node_perspective(doc_blobs)
 
     if (is_theory)
       List(session.header_edit(node_name, header),
diff -r da0513d95155 -r 9b243afbbe83 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 14:07:04 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Feb 27 14:15:23 2014 +0100
@@ -106,6 +106,7 @@
   {
     Swing_Thread.now {
       PIDE.editor.flush()
+      val doc_blobs = document_blobs()
       val init_edits =
         (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
@@ -117,7 +118,7 @@
                   case Some(model) if model.node_name == node_name => (Nil, model)
                   case _ =>
                     val model = Document_Model.init(session, buffer, node_name)
-                    (model.init_edits(), model)
+                    (model.init_edits(doc_blobs), model)
                 }
               for {
                 text_area <- JEdit_Lib.jedit_text_areas(buffer)
@@ -127,7 +128,7 @@
             }
           }
         }
-      session.update(document_blobs(), init_edits)
+      session.update(doc_blobs, init_edits)
     }
   }