src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue Dec 09 21:14:11 2014 +0100 (2014-12-09)
changeset 59122 c1dbcde94cd2
parent 59074 7836d927ffca
permissions -rw-r--r--
tuned signature;
wenzelm@58748
     1
/*  Title:      Tools/jEdit/src/structure_matching.scala
wenzelm@58748
     2
    Author:     Makarius
wenzelm@58748
     3
wenzelm@58748
     4
Structure matcher for Isabelle/Isar outer syntax.
wenzelm@58748
     5
*/
wenzelm@58748
     6
wenzelm@58748
     7
package isabelle.jedit
wenzelm@58748
     8
wenzelm@58748
     9
wenzelm@58748
    10
import isabelle._
wenzelm@58748
    11
wenzelm@58803
    12
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
wenzelm@58748
    13
wenzelm@58748
    14
wenzelm@58748
    15
object Structure_Matching
wenzelm@58748
    16
{
wenzelm@58748
    17
  object Isabelle_Matcher extends StructureMatcher
wenzelm@58748
    18
  {
wenzelm@58803
    19
    private def find_block(
wenzelm@58752
    20
      open: Token => Boolean,
wenzelm@58752
    21
      close: Token => Boolean,
wenzelm@58752
    22
      reset: Token => Boolean,
wenzelm@58762
    23
      restrict: Token => Boolean,
wenzelm@58754
    24
      it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
wenzelm@58752
    25
    {
wenzelm@58754
    26
      val range1 = it.next.range
wenzelm@58762
    27
      it.takeWhile(info => !info.info.is_command || restrict(info.info)).
wenzelm@58762
    28
        scanLeft((range1, 1))(
wenzelm@58762
    29
          { case ((r, d), Text.Info(range, tok)) =>
wenzelm@58762
    30
              if (open(tok)) (range, d + 1)
wenzelm@58762
    31
              else if (close(tok)) (range, d - 1)
wenzelm@58762
    32
              else if (reset(tok)) (range, 0)
wenzelm@58762
    33
              else (r, d) }
wenzelm@58762
    34
        ).collectFirst({ case (range2, 0) => (range1, range2) })
wenzelm@58752
    35
    }
wenzelm@58752
    36
wenzelm@58803
    37
    private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
wenzelm@58748
    38
    {
wenzelm@58748
    39
      val buffer = text_area.getBuffer
wenzelm@58748
    40
      val caret_line = text_area.getCaretLine
wenzelm@58749
    41
      val caret = text_area.getCaretPosition
wenzelm@58748
    42
wenzelm@59074
    43
      Isabelle.buffer_syntax(text_area.getBuffer) match {
wenzelm@58803
    44
        case Some(syntax) =>
wenzelm@58750
    45
          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
wenzelm@58750
    46
wenzelm@58901
    47
          def is_command_kind(token: Token, pred: String => Boolean): Boolean =
wenzelm@59122
    48
            token.is_command_kind(syntax.keywords, pred)
wenzelm@58900
    49
wenzelm@58750
    50
          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58756
    51
            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
wenzelm@58756
    52
              filter(_.info.is_proper)
wenzelm@58750
    53
wenzelm@58750
    54
          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58756
    55
            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
wenzelm@58756
    56
              filter(_.info.is_proper)
wenzelm@58750
    57
wenzelm@58752
    58
          def caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    59
            iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    60
wenzelm@58752
    61
          def rev_caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    62
            rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    63
wenzelm@58756
    64
          iterator(caret_line, 1).find(info => info.range.touches(caret))
wenzelm@58756
    65
          match {
wenzelm@58901
    66
            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) =>
wenzelm@58755
    67
              find_block(
wenzelm@58901
    68
                is_command_kind(_, Keyword.proof_goal),
wenzelm@58901
    69
                is_command_kind(_, Keyword.qed),
wenzelm@58901
    70
                is_command_kind(_, Keyword.qed_global),
wenzelm@58762
    71
                t =>
wenzelm@58901
    72
                  is_command_kind(t, Keyword.diag) ||
wenzelm@58901
    73
                  is_command_kind(t, Keyword.proof),
wenzelm@58755
    74
                caret_iterator())
wenzelm@58755
    75
wenzelm@58901
    76
            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) =>
wenzelm@58755
    77
              find_block(
wenzelm@58901
    78
                is_command_kind(_, Keyword.proof_goal),
wenzelm@58901
    79
                is_command_kind(_, Keyword.qed),
wenzelm@58755
    80
                _ => false,
wenzelm@58762
    81
                t =>
wenzelm@58901
    82
                  is_command_kind(t, Keyword.diag) ||
wenzelm@58901
    83
                  is_command_kind(t, Keyword.proof),
wenzelm@58755
    84
                caret_iterator())
wenzelm@58755
    85
wenzelm@58901
    86
            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) =>
wenzelm@58901
    87
              rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory))
wenzelm@58749
    88
              match {
wenzelm@58750
    89
                case Some(Text.Info(range2, tok))
wenzelm@58901
    90
                if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
wenzelm@58749
    91
                case _ => None
wenzelm@58749
    92
              }
wenzelm@58752
    93
wenzelm@58901
    94
            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) =>
wenzelm@58755
    95
              find_block(
wenzelm@58901
    96
                is_command_kind(_, Keyword.qed),
wenzelm@58755
    97
                t =>
wenzelm@58901
    98
                  is_command_kind(t, Keyword.proof_goal) ||
wenzelm@58901
    99
                  is_command_kind(t, Keyword.theory_goal),
wenzelm@58755
   100
                _ => false,
wenzelm@58762
   101
                t =>
wenzelm@58901
   102
                  is_command_kind(t, Keyword.diag) ||
wenzelm@58901
   103
                  is_command_kind(t, Keyword.proof) ||
wenzelm@58901
   104
                  is_command_kind(t, Keyword.theory_goal),
wenzelm@58755
   105
                rev_caret_iterator())
wenzelm@58755
   106
wenzelm@58752
   107
            case Some(Text.Info(range1, tok)) if tok.is_begin =>
wenzelm@58762
   108
              find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
wenzelm@58752
   109
wenzelm@58752
   110
            case Some(Text.Info(range1, tok)) if tok.is_end =>
wenzelm@58762
   111
              find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
wenzelm@58763
   112
              match {
wenzelm@58763
   113
                case Some((_, range2)) =>
wenzelm@58800
   114
                  rev_caret_iterator().
wenzelm@58800
   115
                    dropWhile(info => info.range != range2).
wenzelm@58800
   116
                    dropWhile(info => info.range == range2).
wenzelm@58800
   117
                    find(info => info.info.is_command || info.info.is_begin)
wenzelm@58763
   118
                  match {
wenzelm@58800
   119
                    case Some(Text.Info(range3, tok)) =>
wenzelm@58901
   120
                      if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3))
wenzelm@58800
   121
                      else Some((range1, range2))
wenzelm@58763
   122
                    case None => None
wenzelm@58763
   123
                  }
wenzelm@58763
   124
                case None => None
wenzelm@58763
   125
              }
wenzelm@58752
   126
wenzelm@58749
   127
            case _ => None
wenzelm@58748
   128
          }
wenzelm@58803
   129
        case None => None
wenzelm@58748
   130
      }
wenzelm@58748
   131
    }
wenzelm@58748
   132
wenzelm@58749
   133
    def getMatch(text_area: TextArea): StructureMatcher.Match =
wenzelm@58749
   134
      find_pair(text_area) match {
wenzelm@58749
   135
        case Some((_, range)) =>
wenzelm@58749
   136
          val line = text_area.getBuffer.getLineOfOffset(range.start)
wenzelm@58749
   137
          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
wenzelm@58749
   138
            line, range.start, line, range.stop)
wenzelm@58749
   139
        case None => null
wenzelm@58749
   140
      }
wenzelm@58749
   141
wenzelm@58748
   142
    def selectMatch(text_area: TextArea)
wenzelm@58748
   143
    {
wenzelm@58803
   144
      def get_span(offset: Text.Offset): Option[Text.Range] =
wenzelm@58803
   145
        for {
wenzelm@59074
   146
          syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
wenzelm@58803
   147
          span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
wenzelm@58803
   148
        } yield span.range
wenzelm@58803
   149
wenzelm@58803
   150
      find_pair(text_area) match {
wenzelm@58803
   151
        case Some((r1, r2)) =>
wenzelm@58803
   152
          (get_span(r1.start), get_span(r2.start)) match {
wenzelm@58803
   153
            case (Some(range1), Some(range2)) =>
wenzelm@58803
   154
              val start = range1.start min range2.start
wenzelm@58803
   155
              val stop = range1.stop max range2.stop
wenzelm@58803
   156
wenzelm@58803
   157
              text_area.moveCaretPosition(stop, false)
wenzelm@58803
   158
              if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
wenzelm@58803
   159
              text_area.addToSelection(new Selection.Range(start, stop))
wenzelm@58803
   160
            case _ =>
wenzelm@58803
   161
          }
wenzelm@58803
   162
        case None =>
wenzelm@58803
   163
      }
wenzelm@58748
   164
    }
wenzelm@58748
   165
  }
wenzelm@58748
   166
}
wenzelm@58748
   167