# HG changeset patch
# User wenzelm
# Date 1406106504 -7200
# Node ID b6256ea3b7c5aa6e2bd9490687a1c6e48bc960ee
# Parent  518e28a7c74b9ec135c73feb220187931406cfdb
proper change of perspective for removed nodes (stemming from closed buffers);

diff -r 518e28a7c74b -r b6256ea3b7c5 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 10:02:19 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:08:24 2014 +0200
@@ -22,12 +22,25 @@
 
   override def session: Session = PIDE.session
 
+  // owned by Swing thread
+  private var removed_nodes = Set.empty[Document.Node.Name]
+
+  def remove_node(name: Document.Node.Name): Unit =
+    Swing_Thread.require { removed_nodes += name }
+
   override def flush()
   {
     Swing_Thread.require {}
 
     val doc_blobs = PIDE.document_blobs()
-    val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_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.empty_perspective_text))
+
+    val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
     if (!edits.isEmpty) session.update(doc_blobs, edits)
   }
 
diff -r 518e28a7c74b -r b6256ea3b7c5 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Jul 23 10:02:19 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 23 11:08:24 2014 +0200
@@ -296,7 +296,14 @@
           PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
 
         case msg: BufferUpdate
-        if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+        if msg.getWhat == BufferUpdate.LOADED ||
+          msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
+          msg.getWhat == BufferUpdate.CLOSING =>
+
+          if (msg.getWhat == BufferUpdate.CLOSING) {
+            val buffer = msg.getBuffer
+            if (buffer != null) PIDE.editor.remove_node(PIDE.resources.node_name(msg.getBuffer))
+          }
           if (PIDE.session.is_ready) {
             delay_init.invoke()
             delay_load.invoke()