author | wenzelm |
Wed, 11 Nov 2020 22:20:57 +0100 | |
changeset 72578 | 3e8395f9093a |
parent 71981 | 0be06f99b210 |
child 72580 | 531a0c44ea3f |
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 |
import java.io.{File => JFile} |
|
11 |
||
12 |
||
13 |
object Build_Doc |
|
14 |
{ |
|
15 |
/* build_doc */ |
|
16 |
||
17 |
def build_doc( |
|
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 | 20 |
all_docs: Boolean = false, |
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 | 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 | 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 | 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 | 31 |
if info.groups.contains("doc") |
32 |
doc = info.options.string("document_variants") |
|
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 | 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 | 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 | 40 |
case Nil => |
56432 | 41 |
case bad => error("No documentation session for " + commas_quote(bad)) |
56429 | 42 |
} |
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 | 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 | 54 |
} |
55 |
} |
|
56 |
||
57 |
||
62838 | 58 |
/* Isabelle tool wrapper */ |
56429 | 59 |
|
64161 | 60 |
val isabelle_tool = |
61 |
Isabelle_Tool("build_doc", "build Isabelle documentation", args => |
|
62 |
{ |
|
63 |
var all_docs = false |
|
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 | 66 |
|
64161 | 67 |
val getopts = |
68 |
Getopts(""" |
|
64310 | 69 |
Usage: isabelle build_doc [OPTIONS] [DOCS ...] |
62435 | 70 |
|
71 |
Options are: |
|
72 |
-a select all documentation sessions |
|
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 | 75 |
|
76 |
Build Isabelle documentation from documentation sessions with |
|
77 |
suitable document_variants entry. |
|
78 |
""", |
|
64310 | 79 |
"a" -> (_ => all_docs = true), |
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 | 82 |
|
64161 | 83 |
val docs = getopts(args) |
62435 | 84 |
|
64161 | 85 |
if (!all_docs && docs.isEmpty) getopts.usage() |
62435 | 86 |
|
64161 | 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 | 93 |
} |