src/Tools/jEdit/src/jedit_editor.scala

   private var removed_nodes = Set.empty[Document.Node.Name]
 
   def remove_node(name: Document.Node.Name): Unit =
     GUI_Thread.require { removed_nodes += name }
 
-  override def flush()
+  override def flush(hidden: Boolean = false)
   {
     GUI_Thread.require {}
 
     val doc_blobs = PIDE.document_blobs()
     val models = PIDE.document_models()

     val removed = removed_nodes; removed_nodes = Set.empty
     val removed_perspective =
       (removed -- models.iterator.map(_.node_name)).toList.map(
         name => (name, Document.Node.no_perspective_text))
 
-    val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
+    val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective
     session.update(doc_blobs, edits)
   }
 
   private val delay_flush =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }