# HG changeset patch # User wenzelm # Date 1413989097 -7200 # Node ID 4fedc5d4b2fe8b695ebe5c7f925f1ee7be71bb8b # Parent b5ecbb1c4dc58eb36e69fba489aaa8b765477c17 restricted scanning; diff -r b5ecbb1c4dc5 -r 4fedc5d4b2fe src/Tools/jEdit/src/structure_matching.scala --- a/src/Tools/jEdit/src/structure_matching.scala Wed Oct 22 11:24:48 2014 +0200 +++ b/src/Tools/jEdit/src/structure_matching.scala Wed Oct 22 16:44:57 2014 +0200 @@ -20,16 +20,18 @@ open: Token => Boolean, close: Token => Boolean, reset: Token => Boolean, + restrict: Token => Boolean, it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] = { val range1 = it.next.range - it.scanLeft((range1, 1))( - { 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 (range2, 0) => (range1, range2) }) + it.takeWhile(info => !info.info.is_command || restrict(info.info)). + scanLeft((range1, 1))( + { 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 (range2, 0) => (range1, range2) }) } def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = @@ -65,6 +67,9 @@ syntax.command_kind(_, Keyword.proof_goal), syntax.command_kind(_, Keyword.qed), syntax.command_kind(_, Keyword.qed_global), + t => + syntax.command_kind(t, Keyword.diag) || + syntax.command_kind(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) => @@ -72,6 +77,9 @@ syntax.command_kind(_, Keyword.proof_goal), syntax.command_kind(_, Keyword.qed), _ => false, + t => + syntax.command_kind(t, Keyword.diag) || + syntax.command_kind(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) => @@ -89,13 +97,17 @@ syntax.command_kind(t, Keyword.proof_goal) || syntax.command_kind(t, Keyword.theory_goal), _ => false, + t => + syntax.command_kind(t, Keyword.diag) || + syntax.command_kind(t, Keyword.proof) || + syntax.command_kind(t, Keyword.theory_goal), rev_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => - find_block(_.is_begin, _.is_end, _ => false, caret_iterator()) + find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_end => - find_block(_.is_end, _.is_begin, _ => false, rev_caret_iterator()) + find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator()) case _ => None }