1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 10:02:19 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:08:24 2014 +0200
     1.3 @@ -22,12 +22,25 @@
     1.4  
     1.5    override def session: Session = PIDE.session
     1.6  
     1.7 +  // owned by Swing thread
     1.8 +  private var removed_nodes = Set.empty[Document.Node.Name]
     1.9 +
    1.10 +  def remove_node(name: Document.Node.Name): Unit =
    1.11 +    Swing_Thread.require { removed_nodes += name }
    1.12 +
    1.13    override def flush()
    1.14    {
    1.15      Swing_Thread.require {}
    1.16  
    1.17      val doc_blobs = PIDE.document_blobs()
    1.18 -    val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
    1.19 +    val models = PIDE.document_models()
    1.20 +
    1.21 +    val removed = removed_nodes; removed_nodes = Set.empty
    1.22 +    val removed_perspective =
    1.23 +      (removed -- models.iterator.map(_.node_name)).toList.map(
    1.24 +        name => (name, Document.Node.empty_perspective_text))
    1.25 +
    1.26 +    val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
    1.27      if (!edits.isEmpty) session.update(doc_blobs, edits)
    1.28    }
    1.29  

     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Jul 23 10:02:19 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 23 11:08:24 2014 +0200
     2.3 @@ -296,7 +296,14 @@
     2.4            PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
     2.5  
     2.6          case msg: BufferUpdate
     2.7 -        if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
     2.8 +        if msg.getWhat == BufferUpdate.LOADED ||
     2.9 +          msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
    2.10 +          msg.getWhat == BufferUpdate.CLOSING =>
    2.11 +
    2.12 +          if (msg.getWhat == BufferUpdate.CLOSING) {
    2.13 +            val buffer = msg.getBuffer
    2.14 +            if (buffer != null) PIDE.editor.remove_node(PIDE.resources.node_name(msg.getBuffer))
    2.15 +          }
    2.16            if (PIDE.session.is_ready) {
    2.17              delay_init.invoke()
    2.18              delay_load.invoke()