src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Wed Oct 22 16:44:57 2014 +0200 (2014-10-22)
changeset 58762 4fedc5d4b2fe
parent 58756 eb5d0c58564d
child 58763 1b943a82d5ed
permissions -rw-r--r--
restricted scanning;
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@58748
    12
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher}
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@58754
    19
    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@58749
    37
    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@58748
    43
      PIDE.session.recent_syntax match {
wenzelm@58750
    44
        case syntax: Outer_Syntax
wenzelm@58750
    45
        if syntax != Outer_Syntax.empty =>
wenzelm@58750
    46
wenzelm@58750
    47
          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
wenzelm@58750
    48
wenzelm@58750
    49
          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58756
    50
            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
wenzelm@58756
    51
              filter(_.info.is_proper)
wenzelm@58750
    52
wenzelm@58750
    53
          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58756
    54
            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
wenzelm@58756
    55
              filter(_.info.is_proper)
wenzelm@58750
    56
wenzelm@58752
    57
          def caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    58
            iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    59
wenzelm@58752
    60
          def rev_caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    61
            rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    62
wenzelm@58756
    63
          iterator(caret_line, 1).find(info => info.range.touches(caret))
wenzelm@58756
    64
          match {
wenzelm@58755
    65
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) =>
wenzelm@58755
    66
              find_block(
wenzelm@58755
    67
                syntax.command_kind(_, Keyword.proof_goal),
wenzelm@58755
    68
                syntax.command_kind(_, Keyword.qed),
wenzelm@58755
    69
                syntax.command_kind(_, Keyword.qed_global),
wenzelm@58762
    70
                t =>
wenzelm@58762
    71
                  syntax.command_kind(t, Keyword.diag) ||
wenzelm@58762
    72
                  syntax.command_kind(t, Keyword.proof),
wenzelm@58755
    73
                caret_iterator())
wenzelm@58755
    74
wenzelm@58755
    75
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) =>
wenzelm@58755
    76
              find_block(
wenzelm@58755
    77
                syntax.command_kind(_, Keyword.proof_goal),
wenzelm@58755
    78
                syntax.command_kind(_, Keyword.qed),
wenzelm@58755
    79
                _ => false,
wenzelm@58762
    80
                t =>
wenzelm@58762
    81
                  syntax.command_kind(t, Keyword.diag) ||
wenzelm@58762
    82
                  syntax.command_kind(t, Keyword.proof),
wenzelm@58755
    83
                caret_iterator())
wenzelm@58755
    84
wenzelm@58750
    85
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
wenzelm@58752
    86
              rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
wenzelm@58749
    87
              match {
wenzelm@58750
    88
                case Some(Text.Info(range2, tok))
wenzelm@58750
    89
                if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
wenzelm@58749
    90
                case _ => None
wenzelm@58749
    91
              }
wenzelm@58752
    92
wenzelm@58755
    93
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) =>
wenzelm@58755
    94
              find_block(
wenzelm@58755
    95
                syntax.command_kind(_, Keyword.qed),
wenzelm@58755
    96
                t =>
wenzelm@58755
    97
                  syntax.command_kind(t, Keyword.proof_goal) ||
wenzelm@58755
    98
                  syntax.command_kind(t, Keyword.theory_goal),
wenzelm@58755
    99
                _ => false,
wenzelm@58762
   100
                t =>
wenzelm@58762
   101
                  syntax.command_kind(t, Keyword.diag) ||
wenzelm@58762
   102
                  syntax.command_kind(t, Keyword.proof) ||
wenzelm@58762
   103
                  syntax.command_kind(t, Keyword.theory_goal),
wenzelm@58755
   104
                rev_caret_iterator())
wenzelm@58755
   105
wenzelm@58752
   106
            case Some(Text.Info(range1, tok)) if tok.is_begin =>
wenzelm@58762
   107
              find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
wenzelm@58752
   108
wenzelm@58752
   109
            case Some(Text.Info(range1, tok)) if tok.is_end =>
wenzelm@58762
   110
              find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
wenzelm@58752
   111
wenzelm@58749
   112
            case _ => None
wenzelm@58748
   113
          }
wenzelm@58749
   114
        case _ => None
wenzelm@58748
   115
      }
wenzelm@58748
   116
    }
wenzelm@58748
   117
wenzelm@58749
   118
    def getMatch(text_area: TextArea): StructureMatcher.Match =
wenzelm@58749
   119
      find_pair(text_area) match {
wenzelm@58749
   120
        case Some((_, range)) =>
wenzelm@58749
   121
          val line = text_area.getBuffer.getLineOfOffset(range.start)
wenzelm@58749
   122
          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
wenzelm@58749
   123
            line, range.start, line, range.stop)
wenzelm@58749
   124
        case None => null
wenzelm@58749
   125
      }
wenzelm@58749
   126
wenzelm@58748
   127
    def selectMatch(text_area: TextArea)
wenzelm@58748
   128
    {
wenzelm@58748
   129
      // FIXME
wenzelm@58748
   130
    }
wenzelm@58748
   131
  }
wenzelm@58748
   132
}
wenzelm@58748
   133