tuned GUI events;
authorwenzelm
Sat, 26 Apr 2014 15:01:42 +0200
changeset 56751 2080e752ed40
parent 56750 205dd4439db1
child 56752 72b4205f4de9
tuned GUI events;
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") {