--- 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"