# HG changeset patch
# User wenzelm
# Date 1413918156 -7200
# Node ID fc822ca2428a749659029a444e4a15a2e25e95a7
# Parent  0232d43422d68e561308110e305b42e15f7f1bb6
support for proof structure matching;

diff -r 0232d43422d6 -r fc822ca2428a src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 20:45:05 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 21:02:36 2014 +0200
@@ -58,6 +58,20 @@
 
           iterator(caret_line, 1).find(info => info.range.touches(caret)) match
           {
+            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) =>
+              find_block(
+                syntax.command_kind(_, Keyword.proof_goal),
+                syntax.command_kind(_, Keyword.qed),
+                syntax.command_kind(_, Keyword.qed_global),
+                caret_iterator())
+
+            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) =>
+              find_block(
+                syntax.command_kind(_, Keyword.proof_goal),
+                syntax.command_kind(_, Keyword.qed),
+                _ => false,
+                caret_iterator())
+
             case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
               rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
               match {
@@ -66,6 +80,15 @@
                 case _ => None
               }
 
+            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) =>
+              find_block(
+                syntax.command_kind(_, Keyword.qed),
+                t =>
+                  syntax.command_kind(t, Keyword.proof_goal) ||
+                  syntax.command_kind(t, Keyword.theory_goal),
+                _ => false,
+                rev_caret_iterator())
+
             case Some(Text.Info(range1, tok)) if tok.is_begin =>
               find_block(_.is_begin, _.is_end, _ => false, caret_iterator())