src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 11:28:33 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 14:12:18 2012 +0100
@@ -111,12 +111,6 @@
       }
     }
 
-    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() }
 
@@ -124,13 +118,25 @@
     {
       Swing_Thread.require()
       pending += edit
-      delay_flush()
+      delay_flush(true)
     }
 
     def update_perspective()
     {
       pending_perspective = true
-      delay_flush()
+      delay_flush(true)
+    }
+
+    def init()
+    {
+      flush()
+      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
+    }
+
+    def exit()
+    {
+      delay_flush(false)
+      flush()
     }
   }
 
@@ -192,7 +198,7 @@
 
   private def deactivate()
   {
-    pending_edits.flush()
+    pending_edits.exit()
     buffer.removeBufferListener(buffer_listener)
     Token_Markup.refresh_buffer(buffer)
   }