src/Tools/jEdit/src/document_model.scala

           last_perspective = new_perspective
           session.edit_node(name, node_header(), new_perspective, edits)
       }
     }
 
+    private val delay_flush =
+      Swing_Thread.delay_last(session.input_delay) { flush() }
+
+    def +=(edit: Text.Edit)
+    {
+      Swing_Thread.require()
+      pending += edit
+      delay_flush(true)
+    }
+
+    def update_perspective()
+    {
+      pending_perspective = true
+      delay_flush(true)
+    }
+
     def init()
     {
       flush()
       session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
     }
 
-    private val delay_flush =
-      Swing_Thread.delay_last(session.input_delay) { flush() }
-
-    def +=(edit: Text.Edit)
-    {
-      Swing_Thread.require()
-      pending += edit
-      delay_flush()
-    }
-
-    def update_perspective()
-    {
-      pending_perspective = true
-      delay_flush()
+    def exit()
+    {
+      delay_flush(false)
+      flush()
     }
   }
 
   def update_perspective()
   {

     Token_Markup.refresh_buffer(buffer)
   }
 
   private def deactivate()
   {
-    pending_edits.flush()
+    pending_edits.exit()
     buffer.removeBufferListener(buffer_listener)
     Token_Markup.refresh_buffer(buffer)
   }
 }