author | wenzelm |
Sat, 27 Jun 2020 11:25:30 +0200 | |
changeset 71981 | 0be06f99b210 |
parent 71896 | ce06d6456cc8 |
child 72578 | 3e8395f9093a |
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, |
|
22 |
docs: List[String] = Nil): Int = |
|
23 |
{ |
|
67026 | 24 |
val sessions_structure = Sessions.load_structure(options) |
56429 | 25 |
val selection = |
26 |
for { |
|
67023 | 27 |
name <- sessions_structure.build_topological_order |
28 |
info = sessions_structure(name) |
|
56429 | 29 |
if info.groups.contains("doc") |
30 |
doc = info.options.string("document_variants") |
|
31 |
if all_docs || docs.contains(doc) |
|
67023 | 32 |
} yield (doc, name) |
56429 | 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 => |
|
56432 | 39 |
case bad => error("No documentation session for " + commas_quote(bad)) |
56429 | 40 |
} |
41 |
||
56432 | 42 |
progress.echo("Build started for documentation " + commas_quote(selected_docs)) |
56429 | 43 |
|
62641 | 44 |
val res1 = |
71981 | 45 |
Build.build(options, |
46 |
selection = Sessions.Selection(requirements = true, sessions = sessions), |
|
71896
ce06d6456cc8
clarified signature --- fit within limit of 22 arguments;
wenzelm
parents:
71726
diff
changeset
|
47 |
progress = progress, build_heap = true, max_jobs = max_jobs) |
62641 | 48 |
if (res1.ok) { |
56429 | 49 |
Isabelle_System.with_tmp_dir("document_output")(output => |
50 |
{ |
|
62641 | 51 |
val res2 = |
56429 | 52 |
Build.build( |
53 |
options.bool.update("browser_info", false). |
|
54 |
string.update("document", "pdf"). |
|
64220 | 55 |
string.update("document_output", output.implode), |
71981 | 56 |
selection = Sessions.Selection(sessions = sessions), |
71896
ce06d6456cc8
clarified signature --- fit within limit of 22 arguments;
wenzelm
parents:
71726
diff
changeset
|
57 |
progress = progress, clean_build = true, max_jobs = max_jobs) |
62641 | 58 |
if (res2.ok) { |
65082 | 59 |
val doc_dir = Path.explode("~~/doc") |
56429 | 60 |
for (doc <- selected_docs) { |
64220 | 61 |
val name = Path.explode(doc + ".pdf") |
62 |
File.copy(output + name, doc_dir + name) |
|
56429 | 63 |
} |
64 |
} |
|
62641 | 65 |
res2.rc |
56429 | 66 |
}) |
67 |
} |
|
62641 | 68 |
else res1.rc |
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() |
102 |
val rc = |
|
103 |
progress.interrupt_handler { |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69277
diff
changeset
|
104 |
build_doc(options, progress, all_docs, max_jobs, docs) |
64161 | 105 |
} |
106 |
sys.exit(rc) |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
67026
diff
changeset
|
107 |
}) |
56429 | 108 |
} |