changeset 37132 | 10ef4da1c314 |
parent 37129 | 4c83696b340e |
child 37186 | 349e9223c685 |
--- 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) {