focus on default component according to jEdit window management;
authorwenzelm
Sun Sep 22 19:50:48 2013 +0200 (2013-09-22)
changeset 53787e64389fe2d2c
parent 53786 064cb0458071
child 53788 b319a0c8b8a2
focus on default component according to jEdit window management;
src/Tools/jEdit/src/dockable.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/dockable.scala	Sun Sep 22 18:42:18 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/dockable.scala	Sun Sep 22 19:50:48 2013 +0200
     1.3 @@ -13,14 +13,17 @@
     1.4  import javax.swing.JPanel
     1.5  
     1.6  import org.gjt.sp.jedit.View
     1.7 -import org.gjt.sp.jedit.gui.DockableWindowManager
     1.8 +import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
     1.9  
    1.10  
    1.11 -class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
    1.12 +class Dockable(view: View, position: String)
    1.13 +  extends JPanel(new BorderLayout) with DefaultFocusComponent
    1.14  {
    1.15    if (position == DockableWindowManager.FLOATING)
    1.16      setPreferredSize(new Dimension(500, 250))
    1.17  
    1.18 +  def focusOnDefaultComponent { requestFocus }
    1.19 +
    1.20    def set_content(c: Component) { add(c, BorderLayout.CENTER) }
    1.21    def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
    1.22  
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 18:42:18 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 19:50:48 2013 +0200
     2.3 @@ -158,4 +158,6 @@
     2.4        query_label, Component.wrap(query), context, limit, allow_dups,
     2.5        process_indicator.component, apply_query, zoom)
     2.6    add(controls.peer, BorderLayout.NORTH)
     2.7 +
     2.8 +  override def focusOnDefaultComponent { query.requestFocus }
     2.9  }
     3.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sun Sep 22 18:42:18 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Sun Sep 22 19:50:48 2013 +0200
     3.3 @@ -178,4 +178,6 @@
     3.4        provers_label, Component.wrap(provers), isar_proofs,
     3.5        process_indicator.component, apply_query, cancel_query, locate_query, zoom)
     3.6    add(controls.peer, BorderLayout.NORTH)
     3.7 +
     3.8 +  override def focusOnDefaultComponent { apply_query.peer.requestFocus }
     3.9  }