equal
deleted
inserted
replaced
100 private val delay_exit = |
100 private val delay_exit = |
101 GUI_Thread.delay_first(Time.seconds(1.0)) |
101 GUI_Thread.delay_first(Time.seconds(1.0)) |
102 { |
102 { |
103 if (can_auto_close) conclude() |
103 if (can_auto_close) conclude() |
104 else { |
104 else { |
105 val button = |
105 val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } } |
106 new Button(if (_return_code == Some(0)) "OK" else "Close") { |
|
107 reactions += { case ButtonClicked(_) => conclude() } |
|
108 } |
|
109 set_actions(button) |
106 set_actions(button) |
110 button.peer.getRootPane.setDefaultButton(button.peer) |
107 button.peer.getRootPane.setDefaultButton(button.peer) |
111 } |
108 } |
112 } |
109 } |
113 |
110 |