Quelle document_structure.scala Sprache: Scala

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

Overall document structure.
*/

package isabelle

import scala.collection.mutable
import scala.annotation.tailrec

object Document_Structure {
  /** general structure **/

  sealed abstract class Document { def length: Int }
  case class Block(name: String, text: String, body: List[Document]) extends Document {
    val length: Int = body.foldLeft(0)(_ + _.length)
  }
  case class Atom(length: Int) extends Document

  def is_theory_command(command: Command): Boolean =
    command.span.is_keyword_kind(kind => Keyword.theory(kind) && !Keyword.theory_end(kind))

  def is_document_command(command: Command): Boolean =
    command.span.is_keyword_kind(Keyword.document)

  def is_diag_command(command: Command): Boolean =
    command.span.is_keyword_kind(Keyword.diag)

  def is_heading_command(command: Command): Boolean =
    proper_heading_level(command).isDefined

  def proper_heading_level(command: Command): Option[Int] =
    command.span.name match {
      case Thy_Header.CHAPTER => Some(0)
      case Thy_Header.SECTION => Some(1)
      case Thy_Header.SUBSECTION => Some(2)
      case Thy_Header.SUBSUBSECTION => Some(3)
      case Thy_Header.PARAGRAPH => Some(4)
      case Thy_Header.SUBPARAGRAPH => Some(5)
      case _ => None
    }

  def heading_level(command: Command): Option[Int] =
    proper_heading_level(command) orElse (if (is_theory_command(command)) Some(6) else None)

  /** context blocks **/

  def parse_blocks(
    syntax: Outer_Syntax,
    node_name: Document.Node.Name,
    text: CharSequence
  ): List[Document] = {
    def is_plain_theory(command: Command): Boolean =
      is_theory_command(command) && !command.span.is_begin && !command.span.is_end

    /* stack operations */

    def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]

    var stack: List[(Command, mutable.ListBuffer[Document])] =
      List((Command.empty, buffer()))

    def open(command: Command): Unit = { stack = (command, buffer()) :: stack }

    def close(): Boolean =
      stack match {
        case (command, body) :: (_, body2) :: _ =>
          body2 += Block(command.span.name, command.source, body.toList)
          stack = stack.tail
          true
        case _ =>
          false
      }

    def flush(): Unit = if (is_plain_theory(stack.head._1)) close()

    def result(): List[Document] = {
      while (close()) { }
      stack.head._2.toList
    }

    def add(command: Command): Unit = {
      if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
      else if (command.span.is_end) { flush(); close() }

      stack.head._2 += Atom(command.source.length)
    }

    /* result structure */

    val spans = syntax.parse_spans(text)
    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span)))
    result()
  }

  /** section headings **/

  trait Item {
    def name: String = ""
    def source: String = ""
    def heading_level: Option[Int] = None
  }

  object No_Item extends Item

  class Sections {
    private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]

    private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
      List((0, No_Item, buffer()))

    @tailrec private def close(level: Int => Boolean): Unit = {
      stack match {
        case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
          body2 += Block(item.name, item.source, body.toList)
          stack = stack.tail
          close(level)
        case _ =>
      }
    }

    def result(): List[Document] = {
      close(_ => true)
      stack.head._3.toList
    }

    def add(item: Item): Unit = {
      item.heading_level match {
        case Some(i) =>
          close(_ > i)
          stack = (i + 1, item, buffer()) :: stack
        case None =>
      }
      stack.head._3 += Atom(item.source.length)
    }
  }

  /* outer syntax sections */

  private class Command_Item(command: Command) extends Item {
    override def name: String = command.span.name
    override def source: String = command.source
    override def heading_level: Option[Int] = Document_Structure.heading_level(command)
  }

  def parse_sections(
    syntax: Outer_Syntax,
    node_name: Document.Node.Name,
    text: CharSequence
  ): List[Document] = {
    val sections = new Sections

    for { span <- syntax.parse_spans(text) } {
      sections.add(
        new Command_Item(Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span)))
    }
    sections.result()
  }

  /* ML sections */

  private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item {
    override def source: String = token.source
    override def heading_level: Option[Int] = level
  }

  def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] = {
    val sections = new Sections
    val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None)

    var context: Scan.Line_Context = Scan.Finished
    for (line <- Library.separated_chunks(_ == '\n', text)) {
      val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context)
      val level =
        toks.filterNot(_.is_space) match {
          case List(tok) if tok.is_comment =>
            val s = tok.source
            if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c))) {
              if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
              else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
              else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
              else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
              else None
            }
            else None
          case _ => None
        }
      if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished)
        toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None)))
      else
        toks.foreach(tok => sections.add(new ML_Item(tok, None)))

      sections.add(nl)
      context = next_context
    }
    sections.result()
  }
}

quality96%

¤ Dauer der Verarbeitung: 0.13 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.