# HG changeset patch
# User wenzelm
# Date 1398517302 -7200
# Node ID 2080e752ed4029d5c40ccd83753fa8655a0b0601
# Parent  205dd4439db19cb0e1d7c1f14442fb535470f934
tuned GUI events;

diff -r 205dd4439db1 -r 2080e752ed40 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 14:59:50 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sat Apr 26 15:01:42 2014 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
-import scala.swing.event.ButtonClicked
+import scala.swing.event.{ButtonClicked, Key, KeyPressed}
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
@@ -117,6 +117,8 @@
     tooltip = "Limit of displayed results"
     verifier = (s: String) =>
       s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
+    listenTo(keys)
+    reactions += { case KeyPressed(_, Key.Enter, 0, _) => clicked }
   }
 
   private val allow_dups = new CheckBox("Duplicates") {