# HG changeset patch
# User wenzelm
# Date 1473932645 -7200
# Node ID b4051d3f4e94a9ef786679b0193a84f9e256bbd3
# Parent  fd73c5dbaad2aaa280e7f8cd5ea3fe5ee05a922e
tuned;

diff -r fd73c5dbaad2 -r b4051d3f4e94 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Sep 14 22:07:11 2016 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Thu Sep 15 11:44:05 2016 +0200
@@ -22,7 +22,7 @@
     Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
 
 
-  /* abbreviations */
+  /* abbrevs */
 
   private val abbrevs_panel = new Abbrevs_Panel
 
@@ -118,6 +118,36 @@
   }
 
 
+  /* search */
+
+  private class Search_Panel extends BorderPanel {
+    val search_field = new TextField(10)
+    val results_panel = new Wrap_Panel
+    layout(search_field) = BorderPanel.Position.North
+    layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
+
+    val search_space =
+      (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
+    val search_delay =
+      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+        val search_words = Word.explode(Word.lowercase(search_field.text))
+        val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
+        val results =
+          for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
+
+        results_panel.contents.clear
+        for (sym <- results.take(search_limit))
+          results_panel.contents += new Symbol_Component(sym, false)
+        if (results.length > search_limit)
+          results_panel.contents +=
+            new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
+        revalidate
+        repaint
+      }
+      search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
+  }
+
+
   /* tabs */
 
   private val group_tabs: TabbedPane = new TabbedPane {
@@ -133,38 +163,14 @@
           }), null)
       })
 
-    val search_field = new TextField(10)
-    val search_page =
-      new TabbedPane.Page("search", new BorderPanel {
-        val results_panel = new Wrap_Panel
-        layout(search_field) = BorderPanel.Position.North
-        layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
-
-        val search_space =
-          (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
-        val search_delay =
-          GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
-            val search_words = Word.explode(Word.lowercase(search_field.text))
-            val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
-            val results =
-              for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
-
-            results_panel.contents.clear
-            for (sym <- results.take(search_limit))
-              results_panel.contents += new Symbol_Component(sym, false)
-            if (results.length > search_limit)
-              results_panel.contents +=
-                new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
-            revalidate
-            repaint
-          }
-          search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
-      }, "Search Symbols")
+    val search_panel = new Search_Panel
+    val search_page = new TabbedPane.Page("search", search_panel, "Search Symbols")
     pages += search_page
 
     listenTo(selection)
     reactions += {
-      case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus
+      case SelectionChanged(_) if selection.page == search_page =>
+        search_panel.search_field.requestFocus
     }
 
     for (page <- pages)