src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue Oct 21 20:19:14 2014 +0200 (2014-10-21)
changeset 58752 2077bc9558cf
parent 58750 1b4b005d73c1
child 58754 0232d43422d6
permissions -rw-r--r--
support for begin/end matching;
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@58752
    19
    def scan_block(
wenzelm@58752
    20
      open: Token => Boolean,
wenzelm@58752
    21
      close: Token => Boolean,
wenzelm@58752
    22
      reset: Token => Boolean,
wenzelm@58752
    23
      init_range: Text.Range,
wenzelm@58752
    24
      init_depth: Int,
wenzelm@58752
    25
      it: Iterator[Text.Info[Token]]): Option[Text.Range] =
wenzelm@58752
    26
    {
wenzelm@58752
    27
      it.scanLeft((init_range, init_depth))(
wenzelm@58752
    28
        { case ((r, d), Text.Info(range, tok)) =>
wenzelm@58752
    29
            if (open(tok)) (range, d + 1)
wenzelm@58752
    30
            else if (close(tok)) (range, d - 1)
wenzelm@58752
    31
            else if (reset(tok)) (range, 0)
wenzelm@58752
    32
            else (r, d) }
wenzelm@58752
    33
      ).collectFirst({ case (r, 0) => r })
wenzelm@58752
    34
    }
wenzelm@58752
    35
wenzelm@58749
    36
    def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
wenzelm@58748
    37
    {
wenzelm@58748
    38
      val buffer = text_area.getBuffer
wenzelm@58748
    39
      val caret_line = text_area.getCaretLine
wenzelm@58749
    40
      val caret = text_area.getCaretPosition
wenzelm@58748
    41
wenzelm@58748
    42
      PIDE.session.recent_syntax match {
wenzelm@58750
    43
        case syntax: Outer_Syntax
wenzelm@58750
    44
        if syntax != Outer_Syntax.empty =>
wenzelm@58750
    45
wenzelm@58750
    46
          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
wenzelm@58750
    47
wenzelm@58750
    48
          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58750
    49
            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
wenzelm@58750
    50
wenzelm@58750
    51
          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58750
    52
            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
wenzelm@58750
    53
wenzelm@58752
    54
          def caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    55
            iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    56
wenzelm@58752
    57
          def rev_caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm@58752
    58
            rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
wenzelm@58752
    59
wenzelm@58752
    60
          iterator(caret_line, 1).find(info => info.range.touches(caret)) match
wenzelm@58752
    61
          {
wenzelm@58750
    62
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
wenzelm@58752
    63
              rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
wenzelm@58749
    64
              match {
wenzelm@58750
    65
                case Some(Text.Info(range2, tok))
wenzelm@58750
    66
                if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
wenzelm@58749
    67
                case _ => None
wenzelm@58749
    68
              }
wenzelm@58752
    69
wenzelm@58752
    70
            case Some(Text.Info(range1, tok)) if tok.is_begin =>
wenzelm@58752
    71
              val it = caret_iterator()
wenzelm@58752
    72
              it.next
wenzelm@58752
    73
              scan_block(_.is_begin, _.is_end, _ => false, range1, 1, it).
wenzelm@58752
    74
                map(range2 => (range1, range2))
wenzelm@58752
    75
wenzelm@58752
    76
            case Some(Text.Info(range1, tok)) if tok.is_end =>
wenzelm@58752
    77
              val it = rev_caret_iterator()
wenzelm@58752
    78
              it.next
wenzelm@58752
    79
              scan_block(_.is_end, _.is_begin, _ => false, range1, 1, it).
wenzelm@58752
    80
                map(range2 => (range1, range2))
wenzelm@58752
    81
wenzelm@58749
    82
            case _ => None
wenzelm@58748
    83
          }
wenzelm@58749
    84
        case _ => None
wenzelm@58748
    85
      }
wenzelm@58748
    86
    }
wenzelm@58748
    87
wenzelm@58749
    88
    def getMatch(text_area: TextArea): StructureMatcher.Match =
wenzelm@58749
    89
      find_pair(text_area) match {
wenzelm@58749
    90
        case Some((_, range)) =>
wenzelm@58749
    91
          val line = text_area.getBuffer.getLineOfOffset(range.start)
wenzelm@58749
    92
          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
wenzelm@58749
    93
            line, range.start, line, range.stop)
wenzelm@58749
    94
        case None => null
wenzelm@58749
    95
      }
wenzelm@58749
    96
wenzelm@58748
    97
    def selectMatch(text_area: TextArea)
wenzelm@58748
    98
    {
wenzelm@58748
    99
      // FIXME
wenzelm@58748
   100
    }
wenzelm@58748
   101
  }
wenzelm@58748
   102
}
wenzelm@58748
   103