src/Tools/jEdit/etc/options

   -- "open/close delay for document tooltips (seconds)"
 
 public option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
-public option jedit_text_overview_limit : int = 100000
+public option jedit_text_overview_limit : int = 65536
   -- "maximum amount of text to visualize in overview column"
 
 public option jedit_symbols_search_limit : int = 50
   -- "maximum number of symbols in search result"