src/Tools/jEdit/src/structure_matching.scala
changeset 58755 fc822ca2428a
parent 58754 0232d43422d6
child 58756 eb5d0c58564d
     1.1 --- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 20:45:05 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 21:02:36 2014 +0200
     1.3 @@ -58,6 +58,20 @@
     1.4  
     1.5            iterator(caret_line, 1).find(info => info.range.touches(caret)) match
     1.6            {
     1.7 +            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) =>
     1.8 +              find_block(
     1.9 +                syntax.command_kind(_, Keyword.proof_goal),
    1.10 +                syntax.command_kind(_, Keyword.qed),
    1.11 +                syntax.command_kind(_, Keyword.qed_global),
    1.12 +                caret_iterator())
    1.13 +
    1.14 +            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) =>
    1.15 +              find_block(
    1.16 +                syntax.command_kind(_, Keyword.proof_goal),
    1.17 +                syntax.command_kind(_, Keyword.qed),
    1.18 +                _ => false,
    1.19 +                caret_iterator())
    1.20 +
    1.21              case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
    1.22                rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
    1.23                match {
    1.24 @@ -66,6 +80,15 @@
    1.25                  case _ => None
    1.26                }
    1.27  
    1.28 +            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) =>
    1.29 +              find_block(
    1.30 +                syntax.command_kind(_, Keyword.qed),
    1.31 +                t =>
    1.32 +                  syntax.command_kind(t, Keyword.proof_goal) ||
    1.33 +                  syntax.command_kind(t, Keyword.theory_goal),
    1.34 +                _ => false,
    1.35 +                rev_caret_iterator())
    1.36 +
    1.37              case Some(Text.Info(range1, tok)) if tok.is_begin =>
    1.38                find_block(_.is_begin, _.is_end, _ => false, caret_iterator())
    1.39