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

Quelle build_doc.scala Sprache: Scala

/*  Title:      Pure/Admin/build_doc.scala
    Author:     Makarius

Build Isabelle documentation.
*/

package isabelle

object Build_Doc {
  /* build_doc */

  def build_doc(
    options: Options,
    progress: Progress = new Progress,
    all_docs: Boolean = false,
    max_jobs: Option[Int] = None,
    sequential: Boolean = false,
    docs: List[String] = Nil,
    view: Boolean = false
  ): Unit = {
    val sessions_structure = Sessions.load_structure(options)
    val selected =
      for {
        session <- sessions_structure.build_topological_order
        info = sessions_structure(session)
        if info.groups.contains("doc")
        doc = info.options.string("document_variants")
        if all_docs || docs.contains(doc)
      } yield (doc, session)

    val documents = selected.map(_._1)
    val selection = Sessions.Selection(sessions = selected.map(_._2))

    docs.filter(doc => !documents.contains(doc)) match {
      case Nil =>
      case bad => error("No documentation session for " + commas_quote(bad))
    }

    progress.echo("Build started for sessions " + commas_quote(selection.sessions))
    val build_results =
      Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).check

    progress.echo("Build started for documentation " + commas_quote(documents))
    val deps = Sessions.load_structure(options + "document").selection_deps(selection)

    val errs =
      Par_List.maps[(String, String), String](
      {
        case (doc, session) =>
          try {
            progress.expose_interrupt()
            progress.echo("Documentation " + quote(doc) + " ...")

            using(Export.open_session_context(build_results.store, deps.background(session))) {
              session_context =>
                Document_Build.build_documents(
                  Document_Build.context(session_context),
                  output_pdf = Some(Path.explode("~~/doc")))
            }
            None
          }
          catch {
            case Exn.Interrupt.ERROR(msg) =>
              val sep = if (msg.contains('\n')) "\n" else " "
              Some("Documentation " + quote(doc) + " failed:" + sep + msg)
          }
      }, selected, sequential = sequential)

    if (errs.nonEmpty) error(cat_lines(errs))

    if (view) {
      for (entry <- Doc.main_contents().entries(name = docs.contains, pdf = true)) {
        entry.view()
      }
    }
  }

  /* Isabelle tool wrapper */

  val isabelle_tool =
    Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here,
      { args =>
        var view = false
        var all_docs = false
        var max_jobs: Option[Int] = None
        var sequential = false
        var options = Options.init()

        val getopts =
          Getopts("""
Usage: isabelle build_doc [OPTIONS] [DOCS ...]

  Options are:
    -V           view explicitly given documents
    -a           select all documentation sessions
    -j INT       maximum number of parallel jobs (default 1)
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    -s           sequential LaTeX jobs

  Build Isabelle documentation from documentation sessions with
  suitable document_variants entry.
""",
            "V" -> (_ => view = true),
            "a" -> (_ => all_docs = true),
            "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
            "o:" -> (arg => options = options + arg),
            "s" -> (_ => sequential = true))

        val docs = getopts(args)

        if (!all_docs && docs.isEmpty) getopts.usage()

        val progress = new Console_Progress()

        progress.interrupt_handler {
          build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs,
            sequential = sequential, docs = docs, view = view)
        }
      })
}

quality93%

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