# HG changeset patch
# User wenzelm
# Date 1380040964 -7200
# Node ID 104a08c2be9ff9e5859d2691bd6198b5fdfbce6d
# Parent  2e4b435e17bc001e5a28e2ee5a5995d43ca489db
focus text field, to capture key events even on Mac OS X look-and-feel;

diff -r 2e4b435e17bc -r 104a08c2be9f src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Sep 24 17:37:45 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Sep 24 18:42:44 2013 +0200
@@ -179,5 +179,5 @@
       process_indicator.component, apply_query, cancel_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
 
-  override def focusOnDefaultComponent { apply_query.peer.requestFocus }
+  override def focusOnDefaultComponent { provers.requestFocus }
 }