# HG changeset patch
# User wenzelm
# Date 1413990285 -7200
# Node ID 1b943a82d5ed132fafb5ca9ab9e8135da6e31168
# Parent  4fedc5d4b2fe8b695ebe5c7f925f1ee7be71bb8b
find main command keyword of 'begin';

diff -r 4fedc5d4b2fe -r 1b943a82d5ed src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Wed Oct 22 16:44:57 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala	Wed Oct 22 17:04:45 2014 +0200
@@ -108,6 +108,18 @@
 
             case Some(Text.Info(range1, tok)) if tok.is_end =>
               find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
+              match {
+                case Some((_, range2)) =>
+                  rev_caret_iterator().dropWhile(info => info.range != range2).
+                    find(info =>
+                      // FIXME more precise keyword category
+                      syntax.command_kind(info.info, Set(Keyword.THY_BEGIN, Keyword.THY_DECL)))
+                  match {
+                    case Some(Text.Info(range3, _)) => Some((range1, range3))
+                    case None => None
+                  }
+                case None => None
+              }
 
             case _ => None
           }