equal
deleted
inserted
replaced
134 |
134 |
135 |
135 |
136 /* resize */ |
136 /* resize */ |
137 |
137 |
138 private val delay_resize = |
138 private val delay_resize = |
139 Swing_Thread.delay_first( |
139 Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
140 Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() } |
|
141 |
140 |
142 addComponentListener(new ComponentAdapter { |
141 addComponentListener(new ComponentAdapter { |
143 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
142 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
144 }) |
143 }) |
145 |
144 |