diff -r 72367327bab2 -r a8b0d3729a69 src/Pure/System/build_dialog.scala --- a/src/Pure/System/build_dialog.scala Wed Dec 05 20:43:02 2012 +0100 +++ b/src/Pure/System/build_dialog.scala Wed Dec 05 21:13:50 2012 +0100 @@ -8,6 +8,9 @@ import java.awt.{GraphicsEnvironment, Point, Font} +import java.awt.event.{KeyEvent, ActionEvent} +import javax.swing.{JButton, AbstractAction, JComponent, KeyStroke} + import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication} import scala.swing.event.ButtonClicked @@ -75,6 +78,14 @@ val button = new Button("Cancel") { reactions += { case ButtonClicked(_) => button_action() } } + + button.peer.getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).put( + KeyStroke.getKeyStroke(KeyEvent.VK_ENTER, 0), "ENTER") + button.peer.getActionMap.put("ENTER", + new AbstractAction { + override def actionPerformed(e: ActionEvent) { button.peer.doClick } + }) + def button_exit(rc: Int) { button.text = if (rc == 0) "OK" else "Exit"