equal
deleted
inserted
replaced
38 |
38 |
39 |
39 |
40 /* resize */ |
40 /* resize */ |
41 |
41 |
42 private val delay_resize = |
42 private val delay_resize = |
43 GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
43 Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } |
44 |
44 |
45 addComponentListener(new ComponentAdapter { |
45 addComponentListener(new ComponentAdapter { |
46 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
46 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
47 override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
47 override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
48 }) |
48 }) |