proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;
--- 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),
--- 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)
}
}