src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue, 21 Oct 2014 17:49:51 +0200
changeset 58749 83b0f633190e
parent 58748 8f92f17d8781
child 58750 1b4b005d73c1
permissions -rw-r--r--
some structure matching, based on line token iterators;
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
  {
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    19
    def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    20
    {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    21
      val buffer = text_area.getBuffer
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    22
      val caret_line = text_area.getCaretLine
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    23
      val caret = text_area.getCaretPosition
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    24
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    25
      PIDE.session.recent_syntax match {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    26
        case syntax: Outer_Syntax if syntax != Outer_Syntax.empty =>
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    27
          Token_Markup.line_token_iterator(syntax, buffer, caret_line).
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    28
            find({ case (tok, r) => r.touches(caret) })
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    29
          match {
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    30
            case Some((tok, range1)) if (syntax.command_kind(tok, Keyword.qed_global)) =>
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    31
              Token_Markup.line_token_reverse_iterator(syntax, buffer, caret_line).
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    32
                dropWhile({ case (_, r) => caret <= r.stop }).
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    33
                find({ case (tok, _) => syntax.command_kind(tok, Keyword.theory) })
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    34
              match {
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    35
                case Some((tok, range2)) if syntax.command_kind(tok, Keyword.theory_goal) =>
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    36
                  Some((range1, range2))
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    37
                case _ => None
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    38
              }
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    39
            case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    40
          }
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    41
        case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    42
      }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    43
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    44
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    45
    def getMatch(text_area: TextArea): StructureMatcher.Match =
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    46
      find_pair(text_area) match {
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    47
        case Some((_, range)) =>
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    48
          val line = text_area.getBuffer.getLineOfOffset(range.start)
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    49
          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    50
            line, range.start, line, range.stop)
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    51
        case None => null
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    52
      }
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
    53
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    54
    def selectMatch(text_area: TextArea)
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    55
    {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    56
      // FIXME
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    57
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    58
  }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    59
}
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    60