equal
deleted
inserted
replaced
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 = |
106 new Button(if (_return_code == Some(0)) "OK" else "Exit") { |
106 new Button(if (_return_code == Some(0)) "OK" else "Close") { |
107 reactions += { case ButtonClicked(_) => conclude() } |
107 reactions += { case ButtonClicked(_) => conclude() } |
108 } |
108 } |
109 set_actions(button) |
109 set_actions(button) |
110 button.peer.getRootPane.setDefaultButton(button.peer) |
110 button.peer.getRootPane.setDefaultButton(button.peer) |
111 } |
111 } |