diff -r 203794e8977d -r 09a4954e7c07 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Sep 14 22:30:10 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Sep 14 22:50:15 2013 +0200
@@ -21,7 +21,7 @@
 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