src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue Oct 21 19:20:48 2014 +0200 (2014-10-21)
changeset 58750 1b4b005d73c1
parent 58749 83b0f633190e
child 58752 2077bc9558cf
permissions -rw-r--r--
added option jedit_structure_limit;
tuned signature;
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@58749
    19
    def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
wenzelm@58748
    20
    {
wenzelm@58748
    21
      val buffer = text_area.getBuffer
wenzelm@58748
    22
      val caret_line = text_area.getCaretLine
wenzelm@58749
    23
      val caret = text_area.getCaretPosition
wenzelm@58748
    24
wenzelm@58748
    25
      PIDE.session.recent_syntax match {
wenzelm@58750
    26
        case syntax: Outer_Syntax
wenzelm@58750
    27
        if syntax != Outer_Syntax.empty =>
wenzelm@58750
    28
wenzelm@58750
    29
          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
wenzelm@58750
    30
wenzelm@58750
    31
          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58750
    32
            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
wenzelm@58750
    33
wenzelm@58750
    34
          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
wenzelm@58750
    35
            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
wenzelm@58750
    36
wenzelm@58750
    37
          iterator(caret_line, 1).find(info => info.range.touches(caret)) match {
wenzelm@58750
    38
            case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
wenzelm@58750
    39
              rev_iterator(caret_line).dropWhile(info => caret <= info.range.stop).
wenzelm@58750
    40
                find(info => syntax.command_kind(info.info, Keyword.theory))
wenzelm@58749
    41
              match {
wenzelm@58750
    42
                case Some(Text.Info(range2, tok))
wenzelm@58750
    43
                if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
wenzelm@58749
    44
                case _ => None
wenzelm@58749
    45
              }
wenzelm@58749
    46
            case _ => None
wenzelm@58748
    47
          }
wenzelm@58749
    48
        case _ => None
wenzelm@58748
    49
      }
wenzelm@58748
    50
    }
wenzelm@58748
    51
wenzelm@58749
    52
    def getMatch(text_area: TextArea): StructureMatcher.Match =
wenzelm@58749
    53
      find_pair(text_area) match {
wenzelm@58749
    54
        case Some((_, range)) =>
wenzelm@58749
    55
          val line = text_area.getBuffer.getLineOfOffset(range.start)
wenzelm@58749
    56
          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
wenzelm@58749
    57
            line, range.start, line, range.stop)
wenzelm@58749
    58
        case None => null
wenzelm@58749
    59
      }
wenzelm@58749
    60
wenzelm@58748
    61
    def selectMatch(text_area: TextArea)
wenzelm@58748
    62
    {
wenzelm@58748
    63
      // FIXME
wenzelm@58748
    64
    }
wenzelm@58748
    65
  }
wenzelm@58748
    66
}
wenzelm@58748
    67