| changeset 53847 | 104a08c2be9f |
| parent 53787 | e64389fe2d2c |
| child 53872 | 6e69f9ca8f1c |
--- 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 } }