src/Pure/Admin/build_doc.scala
author wenzelm
Wed, 11 Nov 2020 22:20:57 +0100
changeset 72578 3e8395f9093a
parent 71981 0be06f99b210
child 72580 531a0c44ea3f
permissions -rw-r--r--
clarified build_doc, based on Present.build_documents;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
     1
/*  Title:      Pure/Admin/build_doc.scala
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     3
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     4
Build Isabelle documentation.
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     5
*/
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     6
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     8
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
     9
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    10
import java.io.{File => JFile}
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    11
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    12
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    13
object Build_Doc
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    14
{
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    15
  /* build_doc */
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    16
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    17
  def build_doc(
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    18
    options: Options,
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 69854
diff changeset
    19
    progress: Progress = new Progress,
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    20
    all_docs: Boolean = false,
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    21
    max_jobs: Int = 1,
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    22
    docs: List[String] = Nil)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    23
  {
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    24
    val store = Sessions.store(options)
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    25
67026
687c822ee5e3 tuned signature;
wenzelm
parents: 67023
diff changeset
    26
    val sessions_structure = Sessions.load_structure(options)
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    27
    val selected =
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    28
      for {
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    29
        session <- sessions_structure.build_topological_order
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    30
        info = sessions_structure(session)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    31
        if info.groups.contains("doc")
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    32
        doc = info.options.string("document_variants")
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    33
        if all_docs || docs.contains(doc)
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    34
      } yield (doc, session)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    35
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    36
    val documents = selected.map(_._1)
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    37
    val selection = Sessions.Selection(sessions = selected.map(_._2))
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    38
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    39
    docs.filter(doc => !documents.contains(doc)) match {
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    40
      case Nil =>
56432
wenzelm
parents: 56430
diff changeset
    41
      case bad => error("No documentation session for " + commas_quote(bad))
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    42
    }
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    43
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    44
    progress.echo("Build started for sessions " + commas_quote(selection.sessions))
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    45
    Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).ok ||
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    46
      error("Build failed")
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    47
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    48
    progress.echo("Build started for documentation " + commas_quote(documents))
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    49
    val doc_options =
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    50
      options + "document=pdf" + "document_output=~~/doc" + "document_output_sources=false"
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    51
    val deps = Sessions.load_structure(doc_options).selection_deps(selection)
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    52
    for (session <- selection.sessions) {
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    53
      Present.build_documents(session, deps, store, progress = progress)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    54
    }
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    55
  }
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    56
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    57
62838
c91ca9935280 prefer internal tool;
wenzelm
parents: 62641
diff changeset
    58
  /* Isabelle tool wrapper */
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    59
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    60
  val isabelle_tool =
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    61
    Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    62
    {
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    63
      var all_docs = false
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    64
      var max_jobs = 1
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69277
diff changeset
    65
      var options = Options.init()
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    66
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    67
      val getopts =
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    68
        Getopts("""
64310
wenzelm
parents: 64220
diff changeset
    69
Usage: isabelle build_doc [OPTIONS] [DOCS ...]
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    70
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    71
  Options are:
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    72
    -a           select all documentation sessions
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    73
    -j INT       maximum number of parallel jobs (default 1)
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69277
diff changeset
    74
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    75
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    76
  Build Isabelle documentation from documentation sessions with
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    77
  suitable document_variants entry.
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    78
""",
64310
wenzelm
parents: 64220
diff changeset
    79
          "a" -> (_ => all_docs = true),
wenzelm
parents: 64220
diff changeset
    80
          "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69277
diff changeset
    81
          "o:" -> (arg => options = options + arg))
62838
c91ca9935280 prefer internal tool;
wenzelm
parents: 62641
diff changeset
    82
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    83
      val docs = getopts(args)
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    84
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    85
      if (!all_docs && docs.isEmpty) getopts.usage()
62435
2c390ad93bc8 moved getopts to Scala;
wenzelm
parents: 61276
diff changeset
    86
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 63805
diff changeset
    87
      val progress = new Console_Progress()
72578
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    88
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    89
      progress.interrupt_handler {
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    90
        build_doc(options, progress, all_docs, max_jobs, docs)
3e8395f9093a clarified build_doc, based on Present.build_documents;
wenzelm
parents: 71981
diff changeset
    91
      }
69277
258bef08b31e support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents: 67026
diff changeset
    92
    })
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents:
diff changeset
    93
}