tuned signature;
authorwenzelm
Tue Nov 19 20:59:05 2013 +0100 (2013-11-19)
changeset 54522761be40990f1
parent 54521 744ea0025e11
child 54523 11087efad95e
tuned signature;
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 20:53:43 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Nov 19 20:59:05 2013 +0100
     1.3 @@ -19,21 +19,12 @@
     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 -    val edits = document_models().flatMap(_.flushed_edits())
    1.21 -    if (!edits.isEmpty) session.update(document_blobs(), edits)
    1.22 +    val edits = PIDE.document_models().flatMap(_.flushed_edits())
    1.23 +    if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
    1.24    }
    1.25  
    1.26    private val delay_flush =
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Nov 19 20:53:43 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Nov 19 20:59:05 2013 +0100
     2.3 @@ -77,6 +77,15 @@
     2.4        if doc_view.isDefined
     2.5      } yield doc_view.get
     2.6  
     2.7 +  def document_models(): List[Document_Model] =
     2.8 +    for {
     2.9 +      buffer <- JEdit_Lib.jedit_buffers().toList
    2.10 +      model <- document_model(buffer)
    2.11 +    } yield model
    2.12 +
    2.13 +  def document_blobs(): Document.Blobs =
    2.14 +    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
    2.15 +
    2.16    def exit_models(buffers: List[Buffer])
    2.17    {
    2.18      Swing_Thread.now {
    2.19 @@ -113,7 +122,7 @@
    2.20              model_edits ::: edits
    2.21            }
    2.22          }
    2.23 -      session.update(PIDE.editor.document_blobs(), init_edits)
    2.24 +      session.update(document_blobs(), init_edits)
    2.25      }
    2.26    }
    2.27