# HG changeset patch
# User wenzelm
# Date 1398525902 -7200
# Node ID 21662be93f4c3a7ba76b3773354e7c670de3e1ae
# Parent  40f8822d6befad0e803061b0e8719c49b011e850
actually observe search limit;

diff -r 40f8822d6bef -r 21662be93f4c src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 17:20:37 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 26 17:25:02 2014 +0200
@@ -70,14 +70,16 @@
 
       val delay_search =
         Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
-          val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
+          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(max_results + 1)
-          for (sym <- results) results_panel.contents += new Symbol_Component(sym)
-          if (results.length > max_results) results_panel.contents += new Label("...")
+              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
         }