Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: fold_handling.scala Sprache: Scala

Original von: Isabelle^©

/*  Title:      Tools/jEdit/src/fold_handling.scala
    Author:     Makarius

Handling of folds within the text structure.
*/

package isabelle.jedit

import isabelle._

import javax.swing.text.Segment

import scala.collection.JavaConverters

import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}

object Fold_Handling
{
  /* input: dynamic line context  */

  class Fold_Handler extends FoldHandler("isabelle")
  {
    override def equals(other: Any): Boolean =
      other match {
        case that: Fold_Handler => true
        case _ => false
      }

    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
      Token_Markup.Line_Context.after(buffer, line).structure.depth max 0

    override def getPrecedingFoldLevels(
      buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
    {
      val structure = Token_Markup.Line_Context.after(buffer, line).structure
      val result =
        if (line > 0 && structure.command)
          Range.inclusive(line - 1, 0, -1).iterator.
            map(i => Token_Markup.Line_Context.after(buffer, i).structure).
            takeWhile(_.improper).map(_ => structure.depth max 0).toList
        else Nil

      if (result.isEmpty) null
      else JavaConverters.seqAsJavaList(result.map(Integer.valueOf))
    }
  }

  /* output: static document rendering */

  class Document_Fold_Handler(private val rendering: JEdit_Rendering)
    extends FoldHandler("isabelle-document")
  {
    override def equals(other: Any): Boolean =
      other match {
        case that: Document_Fold_Handler => this.rendering == that.rendering
        case _ => false
      }

    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
    {
      def depth(i: Text.Offset): Int =
        if (i < 0) 0
        else {
          rendering.fold_depth(Text.Range(i, i + 1)) match {
            case Text.Info(_, d) :: _ => d
            case _ => 0
          }
        }

      if (line <= 0) 0
      else {
        val range = JEdit_Lib.line_range(buffer, line - 1)
        buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
      }
    }
  }
}

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.