equal
deleted
inserted
replaced
146 |
146 |
147 |
147 |
148 /* resize */ |
148 /* resize */ |
149 |
149 |
150 private val delay_resize = |
150 private val delay_resize = |
151 Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() } |
151 Swing_Thread.delay_first( |
|
152 Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } |
152 |
153 |
153 addComponentListener(new ComponentAdapter { |
154 addComponentListener(new ComponentAdapter { |
154 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
155 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
155 }) |
156 }) |
156 |
157 |