src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue, 21 Oct 2014 21:02:36 +0200
changeset 58755 fc822ca2428a
parent 58754 0232d43422d6
child 58756 eb5d0c58564d
permissions -rw-r--r--
support for proof structure matching;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/structure_matching.scala
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     3
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     4
Structure matcher for Isabelle/Isar outer syntax.
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     5
*/
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     6
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     8
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     9
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    10
import isabelle._
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    11
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    12
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher}
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    13
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    14
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    15
object Structure_Matching
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    16
{
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    17
  object Isabelle_Matcher extends StructureMatcher
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    18
  {
58754
wenzelm
parents: 58752
diff changeset
    19
    def find_block(
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    20
      open: Token => Boolean,
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    21
      close: Token => Boolean,
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    22
      reset: Token => Boolean,
58754
wenzelm
parents: 58752
diff changeset
    23
      it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    24
    {
58754
wenzelm
parents: 58752
diff changeset
    25
      val range1 = it.next.range
wenzelm
parents: 58752
diff changeset
    26
      it.scanLeft((range1, 1))(
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    27
        { case ((r, d), Text.Info(range, tok)) =>
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    28
            if (open(tok)) (range, d + 1)
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    29
            else if (close(tok)) (range, d - 1)
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    30
            else if (reset(tok)) (range, 0)
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    31
            else (r, d) }
58754
wenzelm
parents: 58752
diff changeset
    32
      ).collectFirst({ case (range2, 0) => (range1, range2) })
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    33
    }
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    34
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    35
    def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    36
    {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    37
      val buffer = text_area.getBuffer
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    38
      val caret_line = text_area.getCaretLine
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    39
      val caret = text_area.getCaretPosition
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    40
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    41
      PIDE.session.recent_syntax match {
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    42
        case syntax: Outer_Syntax
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    43
        if syntax != Outer_Syntax.empty =>
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    44
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    45
          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    46
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    47
          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    48
            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    49
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    50
          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    51
            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    52
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    53
          def caret_iterator(): Iterator[Text.Info[Token]] =
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    54
            iterator(caret_line).dropWhile(info => !info.range.touches(caret))
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    55
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    56
          def rev_caret_iterator(): Iterator[Text.Info[Token]] =
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    57
            rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    58
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    59
          iterator(caret_line, 1).find(info => info.range.touches(caret)) match
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    60
          {
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    61
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) =>
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    62
              find_block(
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    63
                syntax.command_kind(_, Keyword.proof_goal),
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    64
                syntax.command_kind(_, Keyword.qed),
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    65
                syntax.command_kind(_, Keyword.qed_global),
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    66
                caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    67
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    68
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) =>
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    69
              find_block(
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    70
                syntax.command_kind(_, Keyword.proof_goal),
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    71
                syntax.command_kind(_, Keyword.qed),
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    72
                _ => false,
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    73
                caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    74
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    75
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    76
              rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    77
              match {
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    78
                case Some(Text.Info(range2, tok))
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    79
                if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    80
                case _ => None
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    81
              }
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    82
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    83
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) =>
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    84
              find_block(
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    85
                syntax.command_kind(_, Keyword.qed),
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    86
                t =>
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    87
                  syntax.command_kind(t, Keyword.proof_goal) ||
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    88
                  syntax.command_kind(t, Keyword.theory_goal),
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    89
                _ => false,
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    90
                rev_caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
    91
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    92
            case Some(Text.Info(range1, tok)) if tok.is_begin =>
58754
wenzelm
parents: 58752
diff changeset
    93
              find_block(_.is_begin, _.is_end, _ => false, caret_iterator())
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    94
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    95
            case Some(Text.Info(range1, tok)) if tok.is_end =>
58754
wenzelm
parents: 58752
diff changeset
    96
              find_block(_.is_end, _.is_begin, _ => false, rev_caret_iterator())
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    97
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    98
            case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    99
          }
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   100
        case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   101
      }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   102
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   103
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   104
    def getMatch(text_area: TextArea): StructureMatcher.Match =
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   105
      find_pair(text_area) match {
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   106
        case Some((_, range)) =>
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   107
          val line = text_area.getBuffer.getLineOfOffset(range.start)
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   108
          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   109
            line, range.start, line, range.stop)
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   110
        case None => null
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   111
      }
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   112
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   113
    def selectMatch(text_area: TextArea)
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   114
    {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   115
      // FIXME
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   116
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   117
  }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   118
}
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   119