# HG changeset patch
# User wenzelm
# Date 1354790222 -3600
# Node ID d9711842f1f9ed82db1140fd9a8a8f9354e45f1e
# Parent  b1cb764187607f6ff963237d3016ecefd64ef0a4
clarified default button (cf. org/gjt/sp/jedit/gui/OptionsDialog.java);

diff -r b1cb76418760 -r d9711842f1f9 src/Pure/System/build_dialog.scala
--- a/src/Pure/System/build_dialog.scala	Wed Dec 05 22:25:15 2012 +0100
+++ b/src/Pure/System/build_dialog.scala	Thu Dec 06 11:37:02 2012 +0100
@@ -8,8 +8,6 @@
 
 
 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}
@@ -78,18 +76,11 @@
     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"
       button_action = (() => sys.exit(rc))
+      button.peer.getRootPane.setDefaultButton(button.peer)
     }
 
     val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)