diff -r d4697a30bd02 -r 10ef4da1c314 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 27 12:35:40 2010 +0200
@@ -162,6 +162,7 @@
   /* (re)painting */
 
   private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
+  // FIXME update_delay property
 
   private def update_syntax(cmd: Command)
   {