src/Tools/jEdit/src/jedit_editor.scala
changeset 54521 744ea0025e11
parent 54461 6c360a6ade0e
child 54522 761be40990f1
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 19:43:26 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 20:53:43 2013 +0100
     1.3 @@ -19,21 +19,21 @@
     1.4  
     1.5    override def session: Session = PIDE.session
     1.6  
     1.7 +  def document_models(): List[Document_Model] =
     1.8 +    for {
     1.9 +      buffer <- JEdit_Lib.jedit_buffers().toList
    1.10 +      model <- PIDE.document_model(buffer)
    1.11 +    } yield model
    1.12 +
    1.13 +  def document_blobs(): Document.Blobs =
    1.14 +    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
    1.15 +
    1.16    override def flush()
    1.17    {
    1.18      Swing_Thread.require()
    1.19  
    1.20 -    session.update(
    1.21 -      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    1.22 -        case (edits, buffer) =>
    1.23 -          JEdit_Lib.buffer_lock(buffer) {
    1.24 -            PIDE.document_model(buffer) match {
    1.25 -              case Some(model) => model.flushed_edits() ::: edits
    1.26 -              case None => edits
    1.27 -            }
    1.28 -          }
    1.29 -      }
    1.30 -    )
    1.31 +    val edits = document_models().flatMap(_.flushed_edits())
    1.32 +    if (!edits.isEmpty) session.update(document_blobs(), edits)
    1.33    }
    1.34  
    1.35    private val delay_flush =