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