src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue, 21 Oct 2014 15:21:44 +0200
changeset 58748 8f92f17d8781
child 58749 83b0f633190e
permissions -rw-r--r--
support for structure matching; misc tuning;
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
  {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    19
    def getMatch(text_area: TextArea): StructureMatcher.Match =
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
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    23
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    24
      PIDE.session.recent_syntax match {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    25
        case syntax: Outer_Syntax if syntax != Outer_Syntax.empty =>
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    26
          Token_Markup.buffer_line_tokens(syntax, buffer, caret_line) match {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    27
            case Some(tokens) =>
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    28
              // FIXME
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    29
              null
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    30
            case None => null
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    31
          }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    32
        case _ => null
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    33
      }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    34
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    35
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    36
    def selectMatch(text_area: TextArea)
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    37
    {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    38
      // FIXME
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    39
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    40
  }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    41
}
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    42