# HG changeset patch
# User wenzelm
# Date 1353773526 -3600
# Node ID 0d7f0d8fd63bb6b7d94c53b4be5a25fc32c5e8f9
# Parent  5ab700fd512854dff47287db21e07f49b441ba84
added option jedit_symbols_search_limit;

diff -r 5ab700fd5128 -r 0d7f0d8fd63b src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Nov 24 17:05:10 2012 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Nov 24 17:12:06 2012 +0100
@@ -18,6 +18,9 @@
 option jedit_text_overview_limit : int = 100000
   -- "maximum amount of text to visualize in overview column"
 
+option jedit_symbols_search_limit : int = 50
+  -- "maximum number of symbols in search result"
+
 
 section "Rendering of Document Content"
 
diff -r 5ab700fd5128 -r 0d7f0d8fd63b src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Nov 24 17:05:10 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Nov 24 17:12:06 2012 +0100
@@ -42,10 +42,10 @@
   // FIXME avoid hard-wired stuff
   private val relevant_options =
     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
-      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "threads", "threads_trace",
-      "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay",
-      "editor_input_delay", "editor_output_delay", "editor_reparse_limit", "editor_tracing_limit",
-      "editor_update_delay")
+      "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
+      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
+      "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
+      "editor_tracing_limit", "editor_update_delay")
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
 
diff -r 5ab700fd5128 -r 0d7f0d8fd63b src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 17:05:10 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 17:12:06 2012 +0100
@@ -17,8 +17,6 @@
 
 class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  private val max_results = 50
-
   val searchspace =
     for ((group, symbols) <- Symbol.groups; sym <- symbols)
       yield (sym, sym.toLowerCase)
@@ -70,6 +68,7 @@
       listenTo(search)
       val delay_search =
         Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
+          val max_results = Isabelle.options.int("jedit_symbols_search_limit") max 0
           results_panel.contents.clear
           val results =
             (searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains)