1/*  Title:      Pure/Admin/build_doc.scala
2    Author:     Makarius
3
4Build Isabelle documentation.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12
13object Build_Doc
14{
15  /* build_doc */
16
17  def build_doc(
18    options: Options,
19    progress: Progress = No_Progress,
20    all_docs: Boolean = false,
21    max_jobs: Int = 1,
22    docs: List[String] = Nil): Int =
23  {
24    val sessions_structure = Sessions.load_structure(options)
25    val selection =
26      for {
27        name <- sessions_structure.build_topological_order
28        info = sessions_structure(name)
29        if info.groups.contains("doc")
30        doc = info.options.string("document_variants")
31        if all_docs || docs.contains(doc)
32      } yield (doc, name)
33
34    val selected_docs = selection.map(_._1)
35    val sessions = selection.map(_._2)
36
37    docs.filter(doc => !selected_docs.contains(doc)) match {
38      case Nil =>
39      case bad => error("No documentation session for " + commas_quote(bad))
40    }
41
42    progress.echo("Build started for documentation " + commas_quote(selected_docs))
43
44    val res1 =
45      Build.build(options, progress, requirements = true, build_heap = true,
46        max_jobs = max_jobs, sessions = sessions)
47    if (res1.ok) {
48      Isabelle_System.with_tmp_dir("document_output")(output =>
49        {
50          val res2 =
51            Build.build(
52              options.bool.update("browser_info", false).
53                string.update("document", "pdf").
54                string.update("document_output", output.implode),
55              progress, clean_build = true, max_jobs = max_jobs, sessions = sessions)
56          if (res2.ok) {
57            val doc_dir = Path.explode("~~/doc")
58            for (doc <- selected_docs) {
59              val name = Path.explode(doc + ".pdf")
60              File.copy(output + name, doc_dir + name)
61            }
62          }
63          res2.rc
64        })
65    }
66    else res1.rc
67  }
68
69
70  /* Isabelle tool wrapper */
71
72  val isabelle_tool =
73    Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
74    {
75      var all_docs = false
76      var max_jobs = 1
77      var options = Options.init()
78
79      val getopts =
80        Getopts("""
81Usage: isabelle build_doc [OPTIONS] [DOCS ...]
82
83  Options are:
84    -a           select all documentation sessions
85    -j INT       maximum number of parallel jobs (default 1)
86    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
87
88  Build Isabelle documentation from documentation sessions with
89  suitable document_variants entry.
90""",
91          "a" -> (_ => all_docs = true),
92          "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
93          "o:" -> (arg => options = options + arg))
94
95      val docs = getopts(args)
96
97      if (!all_docs && docs.isEmpty) getopts.usage()
98
99      val progress = new Console_Progress()
100      val rc =
101        progress.interrupt_handler {
102          build_doc(options, progress, all_docs, max_jobs, docs)
103        }
104      sys.exit(rc)
105    })
106}
107