equal
deleted
inserted
replaced
160 |
160 |
161 |
161 |
162 /* (re)painting */ |
162 /* (re)painting */ |
163 |
163 |
164 private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() } |
164 private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() } |
|
165 // FIXME update_delay property |
165 |
166 |
166 private def update_syntax(cmd: Command) |
167 private def update_syntax(cmd: Command) |
167 { |
168 { |
168 val (line1, line2) = model.lines_of_command(document, cmd) |
169 val (line1, line2) = model.lines_of_command(document, cmd) |
169 if (line2 >= text_area.getFirstLine && |
170 if (line2 >= text_area.getFirstLine && |