src/Pure/Admin/build_doc.scala

more robust type, with explicit default;

/*  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)
    if (!build_results.ok) error("Build failed")

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

    val errs =
      Par_List.map[(String, String), Option[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).flatten

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

    if (view) {
      for (doc <- Doc.main_contents().docs if docs.contains(doc.name)) {
        Doc.view(doc.path)
      }
    }
  }


  /* 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)
        }
      })
}