author | wenzelm |
Sat, 05 Mar 2022 20:01:23 +0100 | |
changeset 75225 | 05f677e64178 |
parent 74814 | 79fa9f2d02fa |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
64161 | 1 |
/* Title: Pure/Admin/build_doc.scala |
56429 | 2 |
Author: Makarius |
3 |
||
4 |
Build Isabelle documentation. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Build_Doc |
|
11 |
{ |
|
12 |
/* build_doc */ |
|
13 |
||
14 |
def build_doc( |
|
15 |
options: Options, |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
69854
diff
changeset
|
16 |
progress: Progress = new Progress, |
56429 | 17 |
all_docs: Boolean = false, |
18 |
max_jobs: Int = 1, |
|
73512
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
19 |
sequential: Boolean = false, |
73340 | 20 |
docs: List[String] = Nil): Unit = |
56429 | 21 |
{ |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
22 |
val store = Sessions.store(options) |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
23 |
|
67026 | 24 |
val sessions_structure = Sessions.load_structure(options) |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
25 |
val selected = |
56429 | 26 |
for { |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
27 |
session <- sessions_structure.build_topological_order |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
28 |
info = sessions_structure(session) |
56429 | 29 |
if info.groups.contains("doc") |
30 |
doc = info.options.string("document_variants") |
|
31 |
if all_docs || docs.contains(doc) |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
32 |
} yield (doc, session) |
56429 | 33 |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
34 |
val documents = selected.map(_._1) |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
35 |
val selection = Sessions.Selection(sessions = selected.map(_._2)) |
56429 | 36 |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
37 |
docs.filter(doc => !documents.contains(doc)) match { |
56429 | 38 |
case Nil => |
56432 | 39 |
case bad => error("No documentation session for " + commas_quote(bad)) |
56429 | 40 |
} |
41 |
||
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
42 |
progress.echo("Build started for sessions " + commas_quote(selection.sessions)) |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
43 |
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
|
44 |
error("Build failed") |
56429 | 45 |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
46 |
progress.echo("Build started for documentation " + commas_quote(documents)) |
72675 | 47 |
val doc_options = options + "document=pdf" |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
48 |
val deps = Sessions.load_structure(doc_options).selection_deps(selection) |
72597 | 49 |
|
50 |
val errs = |
|
72675 | 51 |
Par_List.map[(String, String), Option[String]]( |
52 |
{ |
|
53 |
case (doc, session) => |
|
54 |
try { |
|
74814 | 55 |
progress.expose_interrupt() |
72897 | 56 |
progress.echo("Documentation " + quote(doc) + " ...") |
72683 | 57 |
|
72854 | 58 |
using(store.open_database_context())(db_context => |
73719 | 59 |
Document_Build.build_documents(Document_Build.context(session, deps, db_context), |
72685 | 60 |
output_pdf = Some(Path.explode("~~/doc")))) |
72675 | 61 |
None |
62 |
} |
|
63 |
catch { |
|
64 |
case Exn.Interrupt.ERROR(msg) => |
|
65 |
val sep = if (msg.contains('\n')) "\n" else " " |
|
72897 | 66 |
Some("Documentation " + quote(doc) + " failed:" + sep + msg) |
72675 | 67 |
} |
73512
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
68 |
}, selected, sequential = sequential).flatten |
72597 | 69 |
|
70 |
if (errs.nonEmpty) error(cat_lines(errs)) |
|
56429 | 71 |
} |
72 |
||
73 |
||
62838 | 74 |
/* Isabelle tool wrapper */ |
56429 | 75 |
|
64161 | 76 |
val isabelle_tool = |
72763 | 77 |
Isabelle_Tool("build_doc", "build Isabelle documentation", Scala_Project.here, args => |
64161 | 78 |
{ |
79 |
var all_docs = false |
|
80 |
var max_jobs = 1 |
|
73512
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
81 |
var sequential = false |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69277
diff
changeset
|
82 |
var options = Options.init() |
62435 | 83 |
|
64161 | 84 |
val getopts = |
85 |
Getopts(""" |
|
64310 | 86 |
Usage: isabelle build_doc [OPTIONS] [DOCS ...] |
62435 | 87 |
|
88 |
Options are: |
|
89 |
-a select all documentation sessions |
|
90 |
-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
|
91 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
73512
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
92 |
-s sequential LaTeX jobs |
62435 | 93 |
|
94 |
Build Isabelle documentation from documentation sessions with |
|
95 |
suitable document_variants entry. |
|
96 |
""", |
|
64310 | 97 |
"a" -> (_ => all_docs = true), |
98 |
"j:" -> (arg => max_jobs = Value.Int.parse(arg)), |
|
73512
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
99 |
"o:" -> (arg => options = options + arg), |
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
100 |
"s" -> (_ => sequential = true)) |
62838 | 101 |
|
64161 | 102 |
val docs = getopts(args) |
62435 | 103 |
|
64161 | 104 |
if (!all_docs && docs.isEmpty) getopts.usage() |
62435 | 105 |
|
64161 | 106 |
val progress = new Console_Progress() |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
107 |
|
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
108 |
progress.interrupt_handler { |
73512
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
109 |
build_doc(options, progress = progress, all_docs = all_docs, max_jobs = max_jobs, |
e52a9b208481
support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.;
wenzelm
parents:
73340
diff
changeset
|
110 |
sequential = sequential, docs = docs) |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
111 |
} |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
67026
diff
changeset
|
112 |
}) |
56429 | 113 |
} |