equal
deleted
inserted
replaced
142 |
142 |
143 |
143 |
144 /* resize */ |
144 /* resize */ |
145 |
145 |
146 private val delay_resize = |
146 private val delay_resize = |
147 GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
147 Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } |
148 |
148 |
149 addComponentListener(new ComponentAdapter { |
149 addComponentListener(new ComponentAdapter { |
150 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
150 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
151 override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
151 override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
152 }) |
152 }) |