author | wenzelm |
Sun, 22 Nov 2020 13:31:33 +0100 | |
changeset 72685 | a7877e14e7f8 |
parent 72683 | b5e6f0d137a7 |
child 72763 | 3cc73d00553c |
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, |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
19 |
docs: List[String] = Nil) |
56429 | 20 |
{ |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
21 |
val store = Sessions.store(options) |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
22 |
|
67026 | 23 |
val sessions_structure = Sessions.load_structure(options) |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
24 |
val selected = |
56429 | 25 |
for { |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
26 |
session <- sessions_structure.build_topological_order |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
27 |
info = sessions_structure(session) |
56429 | 28 |
if info.groups.contains("doc") |
29 |
doc = info.options.string("document_variants") |
|
30 |
if all_docs || docs.contains(doc) |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
31 |
} yield (doc, session) |
56429 | 32 |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
33 |
val documents = selected.map(_._1) |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
34 |
val selection = Sessions.Selection(sessions = selected.map(_._2)) |
56429 | 35 |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
36 |
docs.filter(doc => !documents.contains(doc)) match { |
56429 | 37 |
case Nil => |
56432 | 38 |
case bad => error("No documentation session for " + commas_quote(bad)) |
56429 | 39 |
} |
40 |
||
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
41 |
progress.echo("Build started for sessions " + commas_quote(selection.sessions)) |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
42 |
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
|
43 |
error("Build failed") |
56429 | 44 |
|
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
45 |
progress.echo("Build started for documentation " + commas_quote(documents)) |
72675 | 46 |
val doc_options = options + "document=pdf" |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
47 |
val deps = Sessions.load_structure(doc_options).selection_deps(selection) |
72597 | 48 |
|
49 |
val errs = |
|
72675 | 50 |
Par_List.map[(String, String), Option[String]]( |
51 |
{ |
|
52 |
case (doc, session) => |
|
53 |
try { |
|
54 |
progress.echo("Documentation " + doc + " ...") |
|
72683 | 55 |
|
56 |
using(store.open_database_context(deps.sessions_structure))(db_context => |
|
57 |
Presentation.build_documents(session, deps, db_context, |
|
72685 | 58 |
output_pdf = Some(Path.explode("~~/doc")))) |
72675 | 59 |
None |
60 |
} |
|
61 |
catch { |
|
62 |
case Exn.Interrupt.ERROR(msg) => |
|
63 |
val sep = if (msg.contains('\n')) "\n" else " " |
|
64 |
Some("Documentation " + doc + " failed:" + sep + msg) |
|
65 |
} |
|
66 |
}, selected).flatten |
|
72597 | 67 |
|
68 |
if (errs.nonEmpty) error(cat_lines(errs)) |
|
56429 | 69 |
} |
70 |
||
71 |
||
62838 | 72 |
/* Isabelle tool wrapper */ |
56429 | 73 |
|
64161 | 74 |
val isabelle_tool = |
75 |
Isabelle_Tool("build_doc", "build Isabelle documentation", args => |
|
76 |
{ |
|
77 |
var all_docs = false |
|
78 |
var max_jobs = 1 |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69277
diff
changeset
|
79 |
var options = Options.init() |
62435 | 80 |
|
64161 | 81 |
val getopts = |
82 |
Getopts(""" |
|
64310 | 83 |
Usage: isabelle build_doc [OPTIONS] [DOCS ...] |
62435 | 84 |
|
85 |
Options are: |
|
86 |
-a select all documentation sessions |
|
87 |
-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
|
88 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
62435 | 89 |
|
90 |
Build Isabelle documentation from documentation sessions with |
|
91 |
suitable document_variants entry. |
|
92 |
""", |
|
64310 | 93 |
"a" -> (_ => all_docs = true), |
94 |
"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
|
95 |
"o:" -> (arg => options = options + arg)) |
62838 | 96 |
|
64161 | 97 |
val docs = getopts(args) |
62435 | 98 |
|
64161 | 99 |
if (!all_docs && docs.isEmpty) getopts.usage() |
62435 | 100 |
|
64161 | 101 |
val progress = new Console_Progress() |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
102 |
|
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
103 |
progress.interrupt_handler { |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
104 |
build_doc(options, progress, all_docs, max_jobs, docs) |
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
71981
diff
changeset
|
105 |
} |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
67026
diff
changeset
|
106 |
}) |
56429 | 107 |
} |