diff -r 944364b48eb9 -r bfed1c26caed src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 11:27:57 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 11:42:51 2014 +0100
@@ -110,12 +110,14 @@
               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)))
+                  rev_caret_iterator().
+                    dropWhile(info => info.range != range2).
+                    dropWhile(info => info.range == range2).
+                    find(info => info.info.is_command || info.info.is_begin)
                   match {
-                    case Some(Text.Info(range3, _)) => Some((range1, range3))
+                    case Some(Text.Info(range3, tok)) =>
+                      if (syntax.command_kind(tok, Keyword.theory_block)) Some((range1, range3))
+                      else Some((range1, range2))
                     case None => None
                   }
                 case None => None