--- 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 =