Quelle line_structure.scala Sprache: Scala

/*  Title:      Pure/Isar/line_structure.scala
    Author:     Makarius

Line-oriented document structure, e.g. for fold handling.
*/

package isabelle

object Line_Structure {
  val init: Line_Structure = Line_Structure()
}

sealed case class Line_Structure(
  improper: Boolean = true,
  blank: Boolean = true,
  command: Boolean = false,
  depth: Int = 0,
  span_depth: Int = 0,
  after_span_depth: Int = 0,
  element_depth: Int = 0
) {
  def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure = {
    val improper1 = tokens.forall(tok => !tok.is_proper)
    val blank1 = tokens.forall(_.is_space)
    val command1 = tokens.exists(_.is_begin_or_command)

    val command_depth =
      tokens.iterator.filter(_.is_proper).nextOption() match {
        case Some(tok) =>
          if (keywords.is_command(tok, Keyword.close_structure))
            Some(after_span_depth - 1)
          else None
        case None => None
      }

    val depth1 =
      if (tokens.exists(tok =>
            keywords.is_before_command(tok) ||
            !tok.is_end && keywords.is_command(tok, Keyword.theory))) element_depth
      else if (command_depth.isDefined) command_depth.get
      else if (command1) after_span_depth
      else span_depth

    val (span_depth1, after_span_depth1, element_depth1) =
      tokens.foldLeft((span_depth, after_span_depth, element_depth)) {
        case (depths @ (x, y, z), tok) =>
          if (tok.is_begin) (z + 2, z + 1, z + 1)
          else if (tok.is_end) (z + 1, z - 1, z - 1)
          else if (tok.is_command) {
            val depth0 = element_depth
            if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
            else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
            else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
            else depths
          }
          else depths
      }

    Line_Structure(
      improper1, blank1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
  }
}

quality100%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.