equal
deleted
inserted
replaced
120 private val delay_resize = |
120 private val delay_resize = |
121 GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
121 GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
122 |
122 |
123 addComponentListener(new ComponentAdapter { |
123 addComponentListener(new ComponentAdapter { |
124 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
124 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
|
125 override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
125 }) |
126 }) |
126 |
127 |
127 |
128 |
128 /* controls */ |
129 /* controls */ |
129 |
130 |