--- a/src/Tools/jEdit/src/structure_matching.scala Wed Oct 22 13:58:30 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala Wed Oct 22 17:34:19 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,29 @@
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())
+ 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
}