src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue Oct 28 16:20:26 2014 +0100 (2014-10-28)
changeset 58803 7a0f675eb671
parent 58800 bfed1c26caed
child 58804 785a65d25790
permissions -rw-r--r--
proper selectMatch, e.g. relevant for S-click on gutter;
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 get_syntax(): Option[Outer_Syntax] =
wenzelm@58803
    20
      PIDE.session.recent_syntax match {
wenzelm@58803
    21
        case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
wenzelm@58803
    22
        case _ => None
wenzelm@58803
    23
      }
wenzelm@58803
    24
wenzelm@58803
    25
    private def find_block(
wenzelm@58752
    26
      open: Token => Boolean,
wenzelm@58752
    27
      close: Token => Boolean,
wenzelm@58752
    28
      reset: Token => Boolean,
wenzelm@58762
    29
      restrict: Token => Boolean,
wenzelm@58754
    30
      it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
wenzelm@58752
    31
    {
wenzelm@58754
    32
      val range1 = it.next.range
wenzelm@58762
    33
      it.takeWhile(info => !info.info.is_command || restrict(info.info)).
wenzelm@58762
    34
        scanLeft((range1, 1))(
wenzelm@58762
    35
          { case ((r, d), Text.Info(range, tok)) =>
wenzelm@58762
    36
              if (open(tok)) (range, d + 1)
wenzelm@58762
    37
              else if (close(tok)) (range, d - 1)
wenzelm@58762
    38
              else if (reset(tok)) (range, 0)
wenzelm@58762
    39
              else (r, d) }
wenzelm@58762
    40
        ).collectFirst({ case (range2, 0) => (range1, range2) })
wenzelm@58752
    41
    }
wenzelm@58752
    42
wenzelm@58803
    43
    private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
wenzelm@58748
    44
    {
wenzelm@58748
    45
      val buffer = text_area.getBuffer
wenzelm@58748
    46
      val caret_line = text_area.getCaretLine
wenzelm@58749
    47
      val caret = text_area.getCaretPosition
wenzelm@58748
    48
wenzelm@58803
    49
      get_syntax() match {
wenzelm@58803
    50
        case Some(syntax) =>
wenzelm@58750
    51
          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
wenzelm@58750
    52
wenzelm@58750
    53
          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58756
    54
            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
wenzelm@58756
    55
              filter(_.info.is_proper)
wenzelm@58750
    56
wenzelm@58750
    57
          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58756
    58
            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
wenzelm@58756
    59
              filter(_.info.is_proper)
wenzelm@58750
    60
wenzelm@58752
    61
          def caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    62
            iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    63
wenzelm@58752
    64
          def rev_caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    65
            rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    66
wenzelm@58756
    67
          iterator(caret_line, 1).find(info => info.range.touches(caret))
wenzelm@58756
    68
          match {
wenzelm@58755
    69
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) =>
wenzelm@58755
    70
              find_block(
wenzelm@58755
    71
                syntax.command_kind(_, Keyword.proof_goal),
wenzelm@58755
    72
                syntax.command_kind(_, Keyword.qed),
wenzelm@58755
    73
                syntax.command_kind(_, Keyword.qed_global),
wenzelm@58762
    74
                t =>
wenzelm@58762
    75
                  syntax.command_kind(t, Keyword.diag) ||
wenzelm@58762
    76
                  syntax.command_kind(t, Keyword.proof),
wenzelm@58755
    77
                caret_iterator())
wenzelm@58755
    78
wenzelm@58755
    79
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) =>
wenzelm@58755
    80
              find_block(
wenzelm@58755
    81
                syntax.command_kind(_, Keyword.proof_goal),
wenzelm@58755
    82
                syntax.command_kind(_, Keyword.qed),
wenzelm@58755
    83
                _ => false,
wenzelm@58762
    84
                t =>
wenzelm@58762
    85
                  syntax.command_kind(t, Keyword.diag) ||
wenzelm@58762
    86
                  syntax.command_kind(t, Keyword.proof),
wenzelm@58755
    87
                caret_iterator())
wenzelm@58755
    88
wenzelm@58750
    89
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
wenzelm@58752
    90
              rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
wenzelm@58749
    91
              match {
wenzelm@58750
    92
                case Some(Text.Info(range2, tok))
wenzelm@58750
    93
                if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
wenzelm@58749
    94
                case _ => None
wenzelm@58749
    95
              }
wenzelm@58752
    96
wenzelm@58755
    97
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) =>
wenzelm@58755
    98
              find_block(
wenzelm@58755
    99
                syntax.command_kind(_, Keyword.qed),
wenzelm@58755
   100
                t =>
wenzelm@58755
   101
                  syntax.command_kind(t, Keyword.proof_goal) ||
wenzelm@58755
   102
                  syntax.command_kind(t, Keyword.theory_goal),
wenzelm@58755
   103
                _ => false,
wenzelm@58762
   104
                t =>
wenzelm@58762
   105
                  syntax.command_kind(t, Keyword.diag) ||
wenzelm@58762
   106
                  syntax.command_kind(t, Keyword.proof) ||
wenzelm@58762
   107
                  syntax.command_kind(t, Keyword.theory_goal),
wenzelm@58755
   108
                rev_caret_iterator())
wenzelm@58755
   109
wenzelm@58752
   110
            case Some(Text.Info(range1, tok)) if tok.is_begin =>
wenzelm@58762
   111
              find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
wenzelm@58752
   112
wenzelm@58752
   113
            case Some(Text.Info(range1, tok)) if tok.is_end =>
wenzelm@58762
   114
              find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
wenzelm@58763
   115
              match {
wenzelm@58763
   116
                case Some((_, range2)) =>
wenzelm@58800
   117
                  rev_caret_iterator().
wenzelm@58800
   118
                    dropWhile(info => info.range != range2).
wenzelm@58800
   119
                    dropWhile(info => info.range == range2).
wenzelm@58800
   120
                    find(info => info.info.is_command || info.info.is_begin)
wenzelm@58763
   121
                  match {
wenzelm@58800
   122
                    case Some(Text.Info(range3, tok)) =>
wenzelm@58800
   123
                      if (syntax.command_kind(tok, Keyword.theory_block)) Some((range1, range3))
wenzelm@58800
   124
                      else Some((range1, range2))
wenzelm@58763
   125
                    case None => None
wenzelm@58763
   126
                  }
wenzelm@58763
   127
                case None => None
wenzelm@58763
   128
              }
wenzelm@58752
   129
wenzelm@58749
   130
            case _ => None
wenzelm@58748
   131
          }
wenzelm@58803
   132
        case None => None
wenzelm@58748
   133
      }
wenzelm@58748
   134
    }
wenzelm@58748
   135
wenzelm@58749
   136
    def getMatch(text_area: TextArea): StructureMatcher.Match =
wenzelm@58749
   137
      find_pair(text_area) match {
wenzelm@58749
   138
        case Some((_, range)) =>
wenzelm@58749
   139
          val line = text_area.getBuffer.getLineOfOffset(range.start)
wenzelm@58749
   140
          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
wenzelm@58749
   141
            line, range.start, line, range.stop)
wenzelm@58749
   142
        case None => null
wenzelm@58749
   143
      }
wenzelm@58749
   144
wenzelm@58748
   145
    def selectMatch(text_area: TextArea)
wenzelm@58748
   146
    {
wenzelm@58803
   147
      def get_span(offset: Text.Offset): Option[Text.Range] =
wenzelm@58803
   148
        for {
wenzelm@58803
   149
          syntax <- get_syntax()
wenzelm@58803
   150
          span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
wenzelm@58803
   151
        } yield span.range
wenzelm@58803
   152
wenzelm@58803
   153
      find_pair(text_area) match {
wenzelm@58803
   154
        case Some((r1, r2)) =>
wenzelm@58803
   155
          (get_span(r1.start), get_span(r2.start)) match {
wenzelm@58803
   156
            case (Some(range1), Some(range2)) =>
wenzelm@58803
   157
              val start = range1.start min range2.start
wenzelm@58803
   158
              val stop = range1.stop max range2.stop
wenzelm@58803
   159
wenzelm@58803
   160
              text_area.moveCaretPosition(stop, false)
wenzelm@58803
   161
              if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
wenzelm@58803
   162
              text_area.addToSelection(new Selection.Range(start, stop))
wenzelm@58803
   163
            case _ =>
wenzelm@58803
   164
          }
wenzelm@58803
   165
        case None =>
wenzelm@58803
   166
      }
wenzelm@58748
   167
    }
wenzelm@58748
   168
  }
wenzelm@58748
   169
}
wenzelm@58748
   170