author | wenzelm |
Fri, 01 Mar 2019 21:29:59 +0100 | |
changeset 69854 | cc0b3e177b49 |
parent 69277 | 258bef08b31e |
child 71726 | a5fda30edae2 |
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, |
|
64909 | 19 |
progress: Progress = No_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 = |
56429 | 45 |
Build.build(options, progress, requirements = true, build_heap = true, |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69277
diff
changeset
|
46 |
max_jobs = max_jobs, sessions = sessions) |
62641 | 47 |
if (res1.ok) { |
56429 | 48 |
Isabelle_System.with_tmp_dir("document_output")(output => |
49 |
{ |
|
62641 | 50 |
val res2 = |
56429 | 51 |
Build.build( |
52 |
options.bool.update("browser_info", false). |
|
53 |
string.update("document", "pdf"). |
|
64220 | 54 |
string.update("document_output", output.implode), |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69277
diff
changeset
|
55 |
progress, clean_build = true, max_jobs = max_jobs, sessions = sessions) |
62641 | 56 |
if (res2.ok) { |
65082 | 57 |
val doc_dir = Path.explode("~~/doc") |
56429 | 58 |
for (doc <- selected_docs) { |
64220 | 59 |
val name = Path.explode(doc + ".pdf") |
60 |
File.copy(output + name, doc_dir + name) |
|
56429 | 61 |
} |
62 |
} |
|
62641 | 63 |
res2.rc |
56429 | 64 |
}) |
65 |
} |
|
62641 | 66 |
else res1.rc |
56429 | 67 |
} |
68 |
||
69 |
||
62838 | 70 |
/* Isabelle tool wrapper */ |
56429 | 71 |
|
64161 | 72 |
val isabelle_tool = |
73 |
Isabelle_Tool("build_doc", "build Isabelle documentation", args => |
|
74 |
{ |
|
75 |
var all_docs = false |
|
76 |
var max_jobs = 1 |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69277
diff
changeset
|
77 |
var options = Options.init() |
62435 | 78 |
|
64161 | 79 |
val getopts = |
80 |
Getopts(""" |
|
64310 | 81 |
Usage: isabelle build_doc [OPTIONS] [DOCS ...] |
62435 | 82 |
|
83 |
Options are: |
|
84 |
-a select all documentation sessions |
|
85 |
-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
|
86 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
62435 | 87 |
|
88 |
Build Isabelle documentation from documentation sessions with |
|
89 |
suitable document_variants entry. |
|
90 |
""", |
|
64310 | 91 |
"a" -> (_ => all_docs = true), |
92 |
"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
|
93 |
"o:" -> (arg => options = options + arg)) |
62838 | 94 |
|
64161 | 95 |
val docs = getopts(args) |
62435 | 96 |
|
64161 | 97 |
if (!all_docs && docs.isEmpty) getopts.usage() |
62435 | 98 |
|
64161 | 99 |
val progress = new Console_Progress() |
100 |
val rc = |
|
101 |
progress.interrupt_handler { |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69277
diff
changeset
|
102 |
build_doc(options, progress, all_docs, max_jobs, docs) |
64161 | 103 |
} |
104 |
sys.exit(rc) |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
67026
diff
changeset
|
105 |
}) |
56429 | 106 |
} |