# HG changeset patch
# User wenzelm
# Date 1413912048 -7200
# Node ID 1b4b005d73c1fab0c5f21044bd8b79596dcac3e9
# Parent  83b0f633190eda8290c5542ec11b6158908ba76a
added option jedit_structure_limit;
tuned signature;

diff -r 83b0f633190e -r 1b4b005d73c1 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"
 
diff -r 83b0f633190e -r 1b4b005d73c1 src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 17:49:51 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 19:20:48 2014 +0200
@@ -23,17 +23,24 @@
       val caret = text_area.getCaretPosition
 
       PIDE.session.recent_syntax match {
-        case syntax: Outer_Syntax if syntax != Outer_Syntax.empty =>
-          Token_Markup.line_token_iterator(syntax, buffer, caret_line).
-            find({ case (tok, r) => r.touches(caret) })
-          match {
-            case Some((tok, range1)) if (syntax.command_kind(tok, Keyword.qed_global)) =>
-              Token_Markup.line_token_reverse_iterator(syntax, buffer, caret_line).
-                dropWhile({ case (_, r) => caret <= r.stop }).
-                find({ case (tok, _) => syntax.command_kind(tok, Keyword.theory) })
+        case syntax: Outer_Syntax
+        if syntax != Outer_Syntax.empty =>
+
+          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
+
+          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
+            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
+
+          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
+            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
+
+          iterator(caret_line, 1).find(info => info.range.touches(caret)) match {
+            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
+              rev_iterator(caret_line).dropWhile(info => caret <= info.range.stop).
+                find(info => syntax.command_kind(info.info, Keyword.theory))
               match {
-                case Some((tok, range2)) if syntax.command_kind(tok, Keyword.theory_goal) =>
-                  Some((range1, range2))
+                case Some(Text.Info(range2, tok))
+                if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
                 case _ => None
               }
             case _ => None
diff -r 83b0f633190e -r 1b4b005d73c1 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Oct 21 17:49:51 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Oct 21 19:20:48 2014 +0200
@@ -225,26 +225,32 @@
   }
 
   def line_token_iterator(
-      syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int): Iterator[(Token, Text.Range)] =
+      syntax: Outer_Syntax,
+      buffer: JEditBuffer,
+      start_line: Int,
+      end_line: Int): Iterator[Text.Info[Token]] =
     for {
-      line <- ((start_line max 0) until buffer.getLineCount).iterator
+      line <- Range(start_line max 0, end_line min buffer.getLineCount).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       starts =
         tokens.iterator.scanLeft(buffer.getLineStartOffset(line))(
           (i, tok) => i + tok.source.length)
-      (tok, i) <- tokens.iterator zip starts
-    } yield (tok, Text.Range(i, i + tok.source.length))
+      (i, tok) <- starts zip tokens.iterator
+    } yield Text.Info(Text.Range(i, i + tok.source.length), tok)
 
   def line_token_reverse_iterator(
-      syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int): Iterator[(Token, Text.Range)] =
+      syntax: Outer_Syntax,
+      buffer: JEditBuffer,
+      start_line: Int,
+      end_line: Int): Iterator[Text.Info[Token]] =
     for {
-      line <- Range.inclusive(start_line min (buffer.getLineCount - 1), 0, -1).iterator
+      line <- Range(start_line min (buffer.getLineCount - 1), end_line max -1, -1).iterator
       tokens <- try_line_tokens(syntax, buffer, line).iterator
       stops =
         tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)(
           (i, tok) => i - tok.source.length)
-      (tok, i) <- tokens.reverseIterator zip stops
-    } yield (tok, Text.Range(i - tok.source.length, i))
+      (i, tok) <- stops zip tokens.reverseIterator
+    } yield Text.Info(Text.Range(i - tok.source.length, i), tok)
 
 
   /* token marker */