# HG changeset patch
# User wenzelm
# Date 1379872248 -7200
# Node ID e64389fe2d2cf16301c49272dfbf7117d8983ae7
# Parent  064cb0458071e880a63f8a1383d3798326dd1e94
focus on default component according to jEdit window management;

diff -r 064cb0458071 -r e64389fe2d2c src/Tools/jEdit/src/dockable.scala
--- a/src/Tools/jEdit/src/dockable.scala	Sun Sep 22 18:42:18 2013 +0200
+++ b/src/Tools/jEdit/src/dockable.scala	Sun Sep 22 19:50:48 2013 +0200
@@ -13,14 +13,17 @@
 import javax.swing.JPanel
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
 
 
-class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
+class Dockable(view: View, position: String)
+  extends JPanel(new BorderLayout) with DefaultFocusComponent
 {
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
+  def focusOnDefaultComponent { requestFocus }
+
   def set_content(c: Component) { add(c, BorderLayout.CENTER) }
   def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
 
diff -r 064cb0458071 -r e64389fe2d2c src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 18:42:18 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 19:50:48 2013 +0200
@@ -158,4 +158,6 @@
       query_label, Component.wrap(query), context, limit, allow_dups,
       process_indicator.component, apply_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
+
+  override def focusOnDefaultComponent { query.requestFocus }
 }
diff -r 064cb0458071 -r e64389fe2d2c src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sun Sep 22 18:42:18 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sun Sep 22 19:50:48 2013 +0200
@@ -178,4 +178,6 @@
       provers_label, Component.wrap(provers), isar_proofs,
       process_indicator.component, apply_query, cancel_query, locate_query, zoom)
   add(controls.peer, BorderLayout.NORTH)
+
+  override def focusOnDefaultComponent { apply_query.peer.requestFocus }
 }