--- 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"
--- 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 _)
--- 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)