src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 19:43:26 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 20:53:43 2013 +0100
@@ -19,21 +19,21 @@
 
   override def session: Session = PIDE.session
 
+  def document_models(): List[Document_Model] =
+    for {
+      buffer <- JEdit_Lib.jedit_buffers().toList
+      model <- PIDE.document_model(buffer)
+    } yield model
+
+  def document_blobs(): Document.Blobs =
+    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
+
   override def flush()
   {
     Swing_Thread.require()
 
-    session.update(
-      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
-        case (edits, buffer) =>
-          JEdit_Lib.buffer_lock(buffer) {
-            PIDE.document_model(buffer) match {
-              case Some(model) => model.flushed_edits() ::: edits
-              case None => edits
-            }
-          }
-      }
-    )
+    val edits = document_models().flatMap(_.flushed_edits())
+    if (!edits.isEmpty) session.update(document_blobs(), edits)
   }
 
   private val delay_flush =