# HG changeset patch
# User wenzelm
# Date 1375867026 -7200
# Node ID 1e22e8101f4714272accc60b4ac9907007540cf4
# Parent  9e4bae21494da989ec7964175402bc164772d4aa
enabled key event to apply query;

diff -r 9e4bae21494d -r 1e22e8101f47 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Wed Aug 07 10:58:26 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Aug 07 11:17:06 2013 +0200
@@ -15,7 +15,7 @@
 import scala.swing.event.ButtonClicked
 
 import java.awt.BorderLayout
-import java.awt.event.{ComponentEvent, ComponentAdapter}
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.gui.HistoryTextField
@@ -91,7 +91,14 @@
 
   /* controls */
 
+  private def clicked { find_theorems.apply_query(List(query.getText)) }
+
   private val query = new HistoryTextField("isabelle-find-theorems") {
+    override def processKeyEvent(evt: KeyEvent)
+    {
+      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
+      super.processKeyEvent(evt)
+    }
     { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
     setColumns(40)
   }
@@ -100,7 +107,7 @@
 
   private val apply_query = new Button("Apply") {
     tooltip = "Find theorems meeting specified criteria"
-    reactions += { case ButtonClicked(_) => find_theorems.apply_query(List(query.getText)) }
+    reactions += { case ButtonClicked(_) => clicked }
   }
 
   private val locate_query = new Button("Locate") {