author | wenzelm |
Tue, 24 Sep 2013 18:42:44 +0200 | |
changeset 53847 | 104a08c2be9f |
parent 53846 | 2e4b435e17bc |
child 53848 | 8d7029eb0c31 |
--- 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 } }