# HG changeset patch
# User wenzelm
# Date 1398527583 -7200
# Node ID f29c9e7a3a8090a9b79004f8dbef8b41f6ea420d
# Parent  21662be93f4c3a7ba76b3773354e7c670de3e1ae
clarified GUI focus;

diff -r 21662be93f4c -r f29c9e7a3a80 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 17:25:02 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 17:53:03 2014 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import scala.swing.event.ValueChanged
+import scala.swing.event.{SelectionChanged, ValueChanged}
 import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
 
 import org.gjt.sp.jedit.View
@@ -59,32 +59,40 @@
             if (group == "control") contents += new Reset_Component
           }), null)
       })
-    pages += new TabbedPane.Page("search", new BorderPanel {
-      val search = new TextField(10)
-      val results_panel = new Wrap_Panel
-      add(search, BorderPanel.Position.North)
-      add(new ScrollPane(results_panel), BorderPanel.Position.Center)
-
-      val search_space =
-        (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
 
-      val delay_search =
-        Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
-          val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
-          results_panel.contents.clear
-          val search_words = Word.explode(Word.lowercase(search.text))
-          val results =
-            (for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym).
-              take(search_limit + 1)
-          for (sym <- results.take(search_limit))
-            results_panel.contents += new Symbol_Component(sym)
-          if (results.length > search_limit)
-            results_panel.contents += new Label("...")
-          revalidate
-          repaint
-        }
-        search.reactions += { case ValueChanged(_) => delay_search.invoke() }
-    }, "Search Symbols")
+    val search_field = new TextField(10)
+    val search_page =
+      new TabbedPane.Page("search", new BorderPanel {
+        val results_panel = new Wrap_Panel
+        add(search_field, BorderPanel.Position.North)
+        add(new ScrollPane(results_panel), BorderPanel.Position.Center)
+  
+        val search_space =
+          (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
+        val delay_search =
+          Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+            val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
+            results_panel.contents.clear
+            val search_words = Word.explode(Word.lowercase(search_field.text))
+            val results =
+              (for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym).
+                take(search_limit + 1)
+            for (sym <- results.take(search_limit))
+              results_panel.contents += new Symbol_Component(sym)
+            if (results.length > search_limit)
+              results_panel.contents += new Label("...")
+            revalidate
+            repaint
+          }
+          search_field.reactions += { case ValueChanged(_) => delay_search.invoke() }
+      }, "Search Symbols")
+    pages += search_page
+
+    listenTo(selection)
+    reactions += {
+      case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus
+    }
+
     pages.map(p =>
       p.title = Word.implode(Word.explode('_', p.title).map(Word.perhaps_capitalize(_))))
   }