Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Pure/Isar/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

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.11 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.