equal
deleted
inserted
replaced
100 _return_code = Some(rc) |
100 _return_code = Some(rc) |
101 delay_exit.invoke |
101 delay_exit.invoke |
102 } |
102 } |
103 |
103 |
104 private val delay_exit = |
104 private val delay_exit = |
105 GUI_Thread.delay_first(Time.seconds(1.0)) |
105 Delay.first(Time.seconds(1.0), gui = true) |
106 { |
106 { |
107 if (can_auto_close) conclude() |
107 if (can_auto_close) conclude() |
108 else { |
108 else { |
109 val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } } |
109 val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } } |
110 set_actions(button) |
110 set_actions(button) |