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