src/Tools/jEdit/src/document_model.scala

 
     def +=(edit: Text.Edit)
     {
       Swing_Thread.require()
       pending += edit
-      delay_flush(true)
+      delay_flush.invoke()
     }
 
     def update_perspective()
     {
-      delay_flush(true)
+      delay_flush.invoke()
     }
 
     def init()
     {
       flush()
       session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
     }
 
     def exit()
     {
-      delay_flush(false)
+      delay_flush.revoke()
       flush()
     }
   }
 
   def update_perspective()