src/Tools/jEdit/src/structure_matching.scala
changeset 58901 47809a811eba
parent 58900 1435cc20b022
child 59074 7836d927ffca
     1.1 --- a/src/Tools/jEdit/src/structure_matching.scala	Wed Nov 05 16:57:12 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/structure_matching.scala	Wed Nov 05 17:37:25 2014 +0100
     1.3 @@ -44,8 +44,8 @@
     1.4          case Some(syntax) =>
     1.5            val limit = PIDE.options.value.int("jedit_structure_limit") max 0
     1.6  
     1.7 -          def command_kind(token: Token, pred: String => Boolean): Boolean =
     1.8 -            syntax.keywords.command_kind(token, pred)
     1.9 +          def is_command_kind(token: Token, pred: String => Boolean): Boolean =
    1.10 +            syntax.keywords.is_command_kind(token, pred)
    1.11  
    1.12            def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    1.13              Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
    1.14 @@ -63,45 +63,45 @@
    1.15  
    1.16            iterator(caret_line, 1).find(info => info.range.touches(caret))
    1.17            match {
    1.18 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.theory_goal) =>
    1.19 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) =>
    1.20                find_block(
    1.21 -                command_kind(_, Keyword.proof_goal),
    1.22 -                command_kind(_, Keyword.qed),
    1.23 -                command_kind(_, Keyword.qed_global),
    1.24 +                is_command_kind(_, Keyword.proof_goal),
    1.25 +                is_command_kind(_, Keyword.qed),
    1.26 +                is_command_kind(_, Keyword.qed_global),
    1.27                  t =>
    1.28 -                  command_kind(t, Keyword.diag) ||
    1.29 -                  command_kind(t, Keyword.proof),
    1.30 +                  is_command_kind(t, Keyword.diag) ||
    1.31 +                  is_command_kind(t, Keyword.proof),
    1.32                  caret_iterator())
    1.33  
    1.34 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.proof_goal) =>
    1.35 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) =>
    1.36                find_block(
    1.37 -                command_kind(_, Keyword.proof_goal),
    1.38 -                command_kind(_, Keyword.qed),
    1.39 +                is_command_kind(_, Keyword.proof_goal),
    1.40 +                is_command_kind(_, Keyword.qed),
    1.41                  _ => false,
    1.42                  t =>
    1.43 -                  command_kind(t, Keyword.diag) ||
    1.44 -                  command_kind(t, Keyword.proof),
    1.45 +                  is_command_kind(t, Keyword.diag) ||
    1.46 +                  is_command_kind(t, Keyword.proof),
    1.47                  caret_iterator())
    1.48  
    1.49 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed_global) =>
    1.50 -              rev_caret_iterator().find(info => command_kind(info.info, Keyword.theory))
    1.51 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) =>
    1.52 +              rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory))
    1.53                match {
    1.54                  case Some(Text.Info(range2, tok))
    1.55 -                if command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
    1.56 +                if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
    1.57                  case _ => None
    1.58                }
    1.59  
    1.60 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed) =>
    1.61 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) =>
    1.62                find_block(
    1.63 -                command_kind(_, Keyword.qed),
    1.64 +                is_command_kind(_, Keyword.qed),
    1.65                  t =>
    1.66 -                  command_kind(t, Keyword.proof_goal) ||
    1.67 -                  command_kind(t, Keyword.theory_goal),
    1.68 +                  is_command_kind(t, Keyword.proof_goal) ||
    1.69 +                  is_command_kind(t, Keyword.theory_goal),
    1.70                  _ => false,
    1.71                  t =>
    1.72 -                  command_kind(t, Keyword.diag) ||
    1.73 -                  command_kind(t, Keyword.proof) ||
    1.74 -                  command_kind(t, Keyword.theory_goal),
    1.75 +                  is_command_kind(t, Keyword.diag) ||
    1.76 +                  is_command_kind(t, Keyword.proof) ||
    1.77 +                  is_command_kind(t, Keyword.theory_goal),
    1.78                  rev_caret_iterator())
    1.79  
    1.80              case Some(Text.Info(range1, tok)) if tok.is_begin =>
    1.81 @@ -117,7 +117,7 @@
    1.82                      find(info => info.info.is_command || info.info.is_begin)
    1.83                    match {
    1.84                      case Some(Text.Info(range3, tok)) =>
    1.85 -                      if (command_kind(tok, Keyword.theory_block)) Some((range1, range3))
    1.86 +                      if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3))
    1.87                        else Some((range1, range2))
    1.88                      case None => None
    1.89                    }