src/Tools/jEdit/etc/options

 option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
 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"
 
 option outdated_color : string = "EEE3E3FF"