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/Build/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle file_format.scala Sprache: Scala

/*  Title:      Pure/Build/file_format.scala
    Author:     Makarius

Support for user-defined file formats, associated with active session.
*/

package isabelle

object File_Format {
  object No_Data extends AnyRef {
    override def toString: String = "File_Format.No_Data"
  }

  sealed case class Theory_Context(name: Document.Node.Name, content: String)

  /* registry */

  lazy val registry: Registry =
    new Registry(Isabelle_System.make_services(classOf[File_Format]))

  final class Registry private [File_Format](file_formats: List[File_Format]) {
    override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")

    def get(name: String): Option[File_Format] = file_formats.find(_.detect(name))
    def get(name: Document.Node.Name): Option[File_Format] = get(name.node)
    def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
    def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined

    def theory_excluded(name: String): Boolean = file_formats.exists(_.theory_excluded(name))

    def parse_data(name: String, text: String): AnyRef =
      get(name) match {
        case Some(file_format) => file_format.parse_data(name, text)
        case None => No_Data
      }
    def parse_data(name: Document.Node.Name, text: String): AnyRef = parse_data(name.node, text)

    def start_session(session: isabelle.Session): Session =
      new Session(file_formats.map(_.start(session)).filterNot(_ == No_Agent))
  }

  /* session */

  final class Session private[File_Format](agents: List[Agent]) {
    override def toString: String =
      agents.mkString("File_Format.Session(", ", ", ")")

    def prover_options(options: Options): Options =
      agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }

    def stop_session(): Unit = agents.foreach(_.stop())
  }

  trait Agent {
    def prover_options(options: Options): Options = options
    def stop(): Unit = {}
  }

  object No_Agent extends Agent
}

abstract class File_Format extends Isabelle_System.Service {
  def format_name: String
  override def toString: String = "File_Format(" + format_name + ")"

  def file_ext: String
  def detect(name: String): Boolean = name.endsWith("." + file_ext)

  def parse_data(name: String, text: String): AnyRef = File_Format.No_Data

  /* implicit theory context: name and content */

  def theory_suffix: String = ""
  def theory_content(name: String): String = ""
  def theory_excluded(name: String): Boolean = false

  def make_theory_name(
    resources: Resources,
    name: Document.Node.Name
  ): Option[Document.Node.Name] = {
    for {
      theory <- Url.get_base_name(name.node)
      if detect(name.node) && theory_suffix.nonEmpty
    }
    yield {
      val node = resources.append_path(name.node, Path.explode(theory_suffix))
      Document.Node.Name(node, theory = theory)
    }
  }

  def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = {
    for {
      prefix <- Url.strip_base_name(thy_name.node)
      suffix <- Url.get_base_name(thy_name.node)
      if detect(prefix) && suffix == theory_suffix
      thy <- Url.get_base_name(prefix)
      s <- proper_string(theory_content(thy))
    } yield s
  }

  def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = None

  /* PIDE session agent */

  def start(session: isabelle.Session): File_Format.Agent = File_Format.No_Agent
}

quality91%

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