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