some structure matching, based on line token iterators;
authorwenzelm
Tue Oct 21 17:49:51 2014 +0200 (2014-10-21 ago)
changeset 5874983b0f633190e
parent 58748 8f92f17d8781
child 58750 1b4b005d73c1
some structure matching, based on line token iterators;
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/structure_matching.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/PIDE/text.scala	Tue Oct 21 15:21:44 2014 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Tue Oct 21 17:49:51 2014 +0200
     1.3 @@ -51,6 +51,8 @@
     1.4      def is_singularity: Boolean = start == stop
     1.5      def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this
     1.6  
     1.7 +    def touches(i: Offset): Boolean = start <= i && i <= stop
     1.8 +
     1.9      def contains(i: Offset): Boolean = start == i || start < i && i < stop
    1.10      def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    1.11      def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
     2.1 --- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 15:21:44 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 17:49:51 2014 +0200
     2.3 @@ -16,23 +16,41 @@
     2.4  {
     2.5    object Isabelle_Matcher extends StructureMatcher
     2.6    {
     2.7 -    def getMatch(text_area: TextArea): StructureMatcher.Match =
     2.8 +    def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
     2.9      {
    2.10        val buffer = text_area.getBuffer
    2.11        val caret_line = text_area.getCaretLine
    2.12 +      val caret = text_area.getCaretPosition
    2.13  
    2.14        PIDE.session.recent_syntax match {
    2.15          case syntax: Outer_Syntax if syntax != Outer_Syntax.empty =>
    2.16 -          Token_Markup.buffer_line_tokens(syntax, buffer, caret_line) match {
    2.17 -            case Some(tokens) =>
    2.18 -              // FIXME
    2.19 -              null
    2.20 -            case None => null
    2.21 +          Token_Markup.line_token_iterator(syntax, buffer, caret_line).
    2.22 +            find({ case (tok, r) => r.touches(caret) })
    2.23 +          match {
    2.24 +            case Some((tok, range1)) if (syntax.command_kind(tok, Keyword.qed_global)) =>
    2.25 +              Token_Markup.line_token_reverse_iterator(syntax, buffer, caret_line).
    2.26 +                dropWhile({ case (_, r) => caret <= r.stop }).
    2.27 +                find({ case (tok, _) => syntax.command_kind(tok, Keyword.theory) })
    2.28 +              match {
    2.29 +                case Some((tok, range2)) if syntax.command_kind(tok, Keyword.theory_goal) =>
    2.30 +                  Some((range1, range2))
    2.31 +                case _ => None
    2.32 +              }
    2.33 +            case _ => None
    2.34            }
    2.35 -        case _ => null
    2.36 +        case _ => None
    2.37        }
    2.38      }
    2.39  
    2.40 +    def getMatch(text_area: TextArea): StructureMatcher.Match =
    2.41 +      find_pair(text_area) match {
    2.42 +        case Some((_, range)) =>
    2.43 +          val line = text_area.getBuffer.getLineOfOffset(range.start)
    2.44 +          new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
    2.45 +            line, range.start, line, range.stop)
    2.46 +        case None => null
    2.47 +      }
    2.48 +
    2.49      def selectMatch(text_area: TextArea)
    2.50      {
    2.51        // FIXME
     3.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Oct 21 15:21:44 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Oct 21 17:49:51 2014 +0200
     3.3 @@ -210,8 +210,10 @@
     3.4        case _ => Line_Context.init
     3.5      }
     3.6  
     3.7 -  def buffer_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
     3.8 -    : Option[List[Token]] =
     3.9 +
    3.10 +  /* line tokens */
    3.11 +
    3.12 +  def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int): Option[List[Token]] =
    3.13    {
    3.14      val line_context =
    3.15        if (line == 0) Line_Context.init
    3.16 @@ -222,6 +224,28 @@
    3.17      } yield syntax.scan_line(text, ctxt)._1
    3.18    }
    3.19  
    3.20 +  def line_token_iterator(
    3.21 +      syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int): Iterator[(Token, Text.Range)] =
    3.22 +    for {
    3.23 +      line <- ((start_line max 0) until buffer.getLineCount).iterator
    3.24 +      tokens <- try_line_tokens(syntax, buffer, line).iterator
    3.25 +      starts =
    3.26 +        tokens.iterator.scanLeft(buffer.getLineStartOffset(line))(
    3.27 +          (i, tok) => i + tok.source.length)
    3.28 +      (tok, i) <- tokens.iterator zip starts
    3.29 +    } yield (tok, Text.Range(i, i + tok.source.length))
    3.30 +
    3.31 +  def line_token_reverse_iterator(
    3.32 +      syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int): Iterator[(Token, Text.Range)] =
    3.33 +    for {
    3.34 +      line <- Range.inclusive(start_line min (buffer.getLineCount - 1), 0, -1).iterator
    3.35 +      tokens <- try_line_tokens(syntax, buffer, line).iterator
    3.36 +      stops =
    3.37 +        tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)(
    3.38 +          (i, tok) => i - tok.source.length)
    3.39 +      (tok, i) <- tokens.reverseIterator zip stops
    3.40 +    } yield (tok, Text.Range(i - tok.source.length, i))
    3.41 +
    3.42  
    3.43    /* token marker */
    3.44