src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 07 13:58:43 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 07 13:58:54 2012 +0200
@@ -121,12 +121,12 @@
     {
       Swing_Thread.require()
       pending += edit
-      delay_flush(true)
+      delay_flush.invoke()
     }
 
     def update_perspective()
     {
-      delay_flush(true)
+      delay_flush.invoke()
     }
 
     def init()
@@ -137,7 +137,7 @@
 
     def exit()
     {
-      delay_flush(false)
+      delay_flush.revoke()
       flush()
     }
   }