support for begin/end matching;

--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 20:18:37 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 20:19:14 2014 +0200
@@ -16,6 +16,23 @@
 {
   object Isabelle_Matcher extends StructureMatcher
   {
+    def scan_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.scanLeft((init_range, init_depth))(
+        { 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 })
+    }
+
     def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
     {
       val buffer = text_area.getBuffer
@@ -34,15 +51,34 @@
           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 {
+          def caret_iterator(): Iterator[Text.Info[Token]] =
+            iterator(caret_line).dropWhile(info => !info.range.touches(caret))
+
+          def rev_caret_iterator(): Iterator[Text.Info[Token]] =
+            rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
+
+          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))
+              rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
               match {
                 case Some(Text.Info(range2, tok))
                 if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
                 case _ => None
               }
+
+            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))
+
+            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))
+
             case _ => None
           }
         case _ => None