src/Tools/jEdit/src/text_structure.scala
author wenzelm
Thu, 07 Jul 2016 21:58:07 +0200
changeset 63425 5a573668ceae
parent 63424 e4e15bbfb3e2
child 63427 88d62f8b5f6e
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
     1
/*  Title:      Tools/jEdit/src/text_structure.scala
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     3
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
     4
Text structure based on Isabelle/Isar outer syntax.
58748
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
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    12
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
    13
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    14
import org.gjt.sp.jedit.buffer.JEditBuffer
63423
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
    15
import org.gjt.sp.jedit.Buffer
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    16
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    17
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    18
object Text_Structure
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    19
{
63425
wenzelm
parents: 63424
diff changeset
    20
  /* token navigator */
wenzelm
parents: 63424
diff changeset
    21
wenzelm
parents: 63424
diff changeset
    22
  class Navigator(syntax: Outer_Syntax, buffer: Buffer)
wenzelm
parents: 63424
diff changeset
    23
  {
wenzelm
parents: 63424
diff changeset
    24
    val limit = PIDE.options.value.int("jedit_structure_limit") max 0
wenzelm
parents: 63424
diff changeset
    25
wenzelm
parents: 63424
diff changeset
    26
    def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm
parents: 63424
diff changeset
    27
      Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
wenzelm
parents: 63424
diff changeset
    28
        filter(_.info.is_proper)
wenzelm
parents: 63424
diff changeset
    29
wenzelm
parents: 63424
diff changeset
    30
    def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm
parents: 63424
diff changeset
    31
      Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
wenzelm
parents: 63424
diff changeset
    32
        filter(_.info.is_proper)
wenzelm
parents: 63424
diff changeset
    33
  }
wenzelm
parents: 63424
diff changeset
    34
wenzelm
parents: 63424
diff changeset
    35
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    36
  /* indentation */
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    37
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    38
  object Indent_Rule extends IndentRule
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    39
  {
63425
wenzelm
parents: 63424
diff changeset
    40
    def apply(buffer: JEditBuffer, line: Int, prev_line: Int, prev_prev_line: Int,
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    41
      actions: java.util.List[IndentAction])
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    42
    {
63425
wenzelm
parents: 63424
diff changeset
    43
      Isabelle.buffer_syntax(buffer) match {
wenzelm
parents: 63424
diff changeset
    44
        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
wenzelm
parents: 63424
diff changeset
    45
          val keywords = syntax.keywords
wenzelm
parents: 63424
diff changeset
    46
          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    47
63425
wenzelm
parents: 63424
diff changeset
    48
          val indent = 0  // FIXME
63423
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
    49
63425
wenzelm
parents: 63424
diff changeset
    50
          actions.clear()
wenzelm
parents: 63424
diff changeset
    51
          actions.add(new IndentAction.AlignOffset(indent))
63423
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
    52
        case _ =>
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
    53
      }
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    54
    }
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    55
  }
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    56
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    57
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    58
  /* structure matching */
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    59
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    60
  object Matcher extends StructureMatcher
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    61
  {
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
    62
    private def find_block(
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    63
      open: Token => Boolean,
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    64
      close: Token => Boolean,
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    65
      reset: Token => Boolean,
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    66
      restrict: Token => Boolean,
58754
wenzelm
parents: 58752
diff changeset
    67
      it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    68
    {
58754
wenzelm
parents: 58752
diff changeset
    69
      val range1 = it.next.range
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    70
      it.takeWhile(info => !info.info.is_command || restrict(info.info)).
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    71
        scanLeft((range1, 1))(
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    72
          { case ((r, d), Text.Info(range, tok)) =>
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    73
              if (open(tok)) (range, d + 1)
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    74
              else if (close(tok)) (range, d - 1)
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    75
              else if (reset(tok)) (range, 0)
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    76
              else (r, d) }
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
    77
        ).collectFirst({ case (range2, 0) => (range1, range2) })
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    78
    }
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    79
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
    80
    private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    81
    {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    82
      val buffer = text_area.getBuffer
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    83
      val caret_line = text_area.getCaretLine
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    84
      val caret = text_area.getCaretPosition
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    85
59074
7836d927ffca tuned signature;
wenzelm
parents: 58901
diff changeset
    86
      Isabelle.buffer_syntax(text_area.getBuffer) match {
63425
wenzelm
parents: 63424
diff changeset
    87
        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
    88
          val keywords = syntax.keywords
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    89
63425
wenzelm
parents: 63424
diff changeset
    90
          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
    91
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    92
          def caret_iterator(): Iterator[Text.Info[Token]] =
63425
wenzelm
parents: 63424
diff changeset
    93
            nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
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
          def rev_caret_iterator(): Iterator[Text.Info[Token]] =
63425
wenzelm
parents: 63424
diff changeset
    96
            nav.rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
    97
63425
wenzelm
parents: 63424
diff changeset
    98
          nav.iterator(caret_line, 1).find(info => info.range.touches(caret))
58756
eb5d0c58564d ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents: 58755
diff changeset
    99
          match {
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   100
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) =>
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   101
              find_block(
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   102
                keywords.is_command(_, Keyword.proof_goal),
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   103
                keywords.is_command(_, Keyword.qed),
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   104
                keywords.is_command(_, Keyword.qed_global),
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   105
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   106
                  keywords.is_command(t, Keyword.diag) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   107
                  keywords.is_command(t, Keyword.proof),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   108
                caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   109
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   110
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) =>
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   111
              find_block(
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   112
                keywords.is_command(_, Keyword.proof_goal),
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   113
                keywords.is_command(_, Keyword.qed),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   114
                _ => false,
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   115
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   116
                  keywords.is_command(t, Keyword.diag) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   117
                  keywords.is_command(t, Keyword.proof),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   118
                caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   119
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   120
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) =>
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   121
              rev_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory))
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   122
              match {
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
   123
                case Some(Text.Info(range2, tok))
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   124
                if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2))
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   125
                case _ => None
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   126
              }
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   127
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   128
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) =>
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   129
              find_block(
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   130
                keywords.is_command(_, Keyword.qed),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   131
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   132
                  keywords.is_command(t, Keyword.proof_goal) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   133
                  keywords.is_command(t, Keyword.theory_goal),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   134
                _ => false,
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   135
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   136
                  keywords.is_command(t, Keyword.diag) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   137
                  keywords.is_command(t, Keyword.proof) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   138
                  keywords.is_command(t, Keyword.theory_goal),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   139
                rev_caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   140
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   141
            case Some(Text.Info(range1, tok)) if tok.is_begin =>
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   142
              find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   143
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   144
            case Some(Text.Info(range1, tok)) if tok.is_end =>
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   145
              find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
58763
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   146
              match {
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   147
                case Some((_, range2)) =>
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   148
                  rev_caret_iterator().
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   149
                    dropWhile(info => info.range != range2).
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   150
                    dropWhile(info => info.range == range2).
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   151
                    find(info => info.info.is_command || info.info.is_begin)
58763
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   152
                  match {
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   153
                    case Some(Text.Info(range3, tok)) =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   154
                      if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3))
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   155
                      else Some((range1, range2))
58763
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   156
                    case None => None
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   157
                  }
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   158
                case None => None
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   159
              }
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   160
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   161
            case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   162
          }
63425
wenzelm
parents: 63424
diff changeset
   163
        case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   164
      }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   165
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   166
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   167
    def getMatch(text_area: TextArea): StructureMatcher.Match =
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   168
      find_pair(text_area) match {
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   169
        case Some((_, range)) =>
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   170
          val line = text_area.getBuffer.getLineOfOffset(range.start)
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   171
          new StructureMatcher.Match(Matcher, line, range.start, line, range.stop)
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   172
        case None => null
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   173
      }
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   174
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   175
    def selectMatch(text_area: TextArea)
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   176
    {
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   177
      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
   178
        for {
59074
7836d927ffca tuned signature;
wenzelm
parents: 58901
diff changeset
   179
          syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   180
          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
   181
        } yield span.range
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   182
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   183
      find_pair(text_area) match {
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   184
        case Some((r1, r2)) =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   185
          (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
   186
            case (Some(range1), Some(range2)) =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   187
              val start = range1.start min range2.start
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   188
              val stop = range1.stop max range2.stop
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   189
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   190
              text_area.moveCaretPosition(stop, false)
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   191
              if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   192
              text_area.addToSelection(new Selection.Range(start, stop))
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   193
            case _ =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   194
          }
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   195
        case None =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   196
      }
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   197
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   198
  }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   199
}