# HG changeset patch
# User wenzelm
# Date 1413917105 -7200
# Node ID 0232d43422d68e561308110e305b42e15f7f1bb6
# Parent  960bf499ca5de1d27a91bf7914454681f7446aa9
tuned;

diff -r 960bf499ca5d -r 0232d43422d6 src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 20:44:17 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 20:45:05 2014 +0200
@@ -16,21 +16,20 @@
 {
   object Isabelle_Matcher extends StructureMatcher
   {
-    def scan_block(
+    def find_block(
       open: Token => Boolean,
       close: Token => Boolean,
       reset: Token => Boolean,
-      init_range: Text.Range,
-      init_depth: Int,
-      it: Iterator[Text.Info[Token]]): Option[Text.Range] =
+      it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
     {
-      it.scanLeft((init_range, init_depth))(
+      val range1 = it.next.range
+      it.scanLeft((range1, 1))(
         { case ((r, d), Text.Info(range, tok)) =>
             if (open(tok)) (range, d + 1)
             else if (close(tok)) (range, d - 1)
             else if (reset(tok)) (range, 0)
             else (r, d) }
-      ).collectFirst({ case (r, 0) => r })
+      ).collectFirst({ case (range2, 0) => (range1, range2) })
     }
 
     def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
@@ -68,16 +67,10 @@
               }
 
             case Some(Text.Info(range1, tok)) if tok.is_begin =>
-              val it = caret_iterator()
-              it.next
-              scan_block(_.is_begin, _.is_end, _ => false, range1, 1, it).
-                map(range2 => (range1, range2))
+              find_block(_.is_begin, _.is_end, _ => false, caret_iterator())
 
             case Some(Text.Info(range1, tok)) if tok.is_end =>
-              val it = rev_caret_iterator()
-              it.next
-              scan_block(_.is_end, _.is_begin, _ => false, range1, 1, it).
-                map(range2 => (range1, range2))
+              find_block(_.is_end, _.is_begin, _ => false, rev_caret_iterator())
 
             case _ => None
           }