src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Tue Oct 21 17:49:51 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Oct 21 19:20:48 2014 +0200
@@ -30,6 +30,9 @@
 public option jedit_text_overview_limit : int = 65536
   -- "maximum amount of text to visualize in overview column"
 
+public option jedit_structure_limit : int = 1000
+  -- "maximum number of lines to scan for language structure"
+
 public option jedit_symbols_search_limit : int = 50
   -- "maximum number of symbols in search result"