equal
deleted
inserted
replaced
33 |
33 |
34 |
34 |
35 /* resize */ |
35 /* resize */ |
36 |
36 |
37 private val delay_resize = |
37 private val delay_resize = |
38 Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } |
38 Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } |
39 |
39 |
40 addComponentListener(new ComponentAdapter { |
40 addComponentListener(new ComponentAdapter { |
41 override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
41 override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
42 override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() |
42 override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() |
43 }) |
43 }) |