--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Feb 27 14:07:04 2014 +0100
@@ -26,17 +26,9 @@
{
Swing_Thread.require()
- val models = PIDE.document_models()
- val changed_blobs =
- (for {
- model <- models.iterator
- if !model.is_theory && model.has_pending_edits
- } yield model.node_name).toSet
-
- System.console.writer.println("\nchanged_blobs = " + changed_blobs)
-
- val edits = models.flatMap(_.flushed_edits(changed_blobs))
- if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
+ val doc_blobs = PIDE.document_blobs()
+ val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
+ if (!edits.isEmpty) session.update(doc_blobs, edits)
}
private val delay_flush =