src/Tools/jEdit/src/jedit_editor.scala
changeset 61728 5f5ff1eab407
parent 61660 78b371644654
child 62062 ee610059b0e9
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Nov 21 20:12:36 2015 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Nov 21 20:13:52 2015 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    def remove_node(name: Document.Node.Name): Unit =
     1.5      GUI_Thread.require { removed_nodes += name }
     1.6  
     1.7 -  override def flush()
     1.8 +  override def flush(hidden: Boolean = false)
     1.9    {
    1.10      GUI_Thread.require {}
    1.11  
    1.12 @@ -40,7 +40,7 @@
    1.13        (removed -- models.iterator.map(_.node_name)).toList.map(
    1.14          name => (name, Document.Node.no_perspective_text))
    1.15  
    1.16 -    val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
    1.17 +    val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective
    1.18      session.update(doc_blobs, edits)
    1.19    }
    1.20