src/Tools/jEdit/src/jedit_editor.scala
changeset 55781 b3a4207fb9a6
parent 55432 9c53198dbb1c
child 55783 da0513d95155
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Feb 27 10:59:12 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Feb 27 12:37:43 2014 +0100
     1.3 @@ -26,7 +26,16 @@
     1.4    {
     1.5      Swing_Thread.require()
     1.6  
     1.7 -    val edits = PIDE.document_models().flatMap(_.flushed_edits())
     1.8 +    val models = PIDE.document_models()
     1.9 +    val changed_blobs =
    1.10 +      (for {
    1.11 +        model <- models.iterator
    1.12 +        if !model.is_theory && model.has_pending_edits
    1.13 +      } yield model.node_name).toSet
    1.14 +
    1.15 +    System.console.writer.println("\nchanged_blobs = " + changed_blobs)
    1.16 +
    1.17 +    val edits = models.flatMap(_.flushed_edits(changed_blobs))
    1.18      if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
    1.19    }
    1.20