# HG changeset patch
# User wenzelm
# Date 1398528381 -7200
# Node ID a18c76b7b299c74e989b84a3c4a2b26562aed5d3
# Parent  f29c9e7a3a8090a9b79004f8dbef8b41f6ea420d
tuned;

diff -r f29c9e7a3a80 -r a18c76b7b299 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 17:53:03 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 18:06:21 2014 +0200
@@ -50,7 +50,7 @@
     tooltip = "Reset control symbols within text"
   }
 
-  val group_tabs: TabbedPane = new TabbedPane {
+  private val group_tabs: TabbedPane = new TabbedPane {
     pages ++=
       Symbol.groups.map({ case (group, symbols) =>
         new TabbedPane.Page(group,
@@ -71,16 +71,17 @@
           (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_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
-            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("...")
+              results_panel.contents +=
+                new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
             revalidate
             repaint
           }
@@ -93,8 +94,8 @@
       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(_))))
+    for (page <- pages)
+      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
   }
   set_content(group_tabs)
 }