| author | wenzelm | 
| Tue, 08 Sep 2015 13:40:37 +0200 | |
| changeset 61132 | 70029aae9a9f | 
| parent 56432 | 96b54a96b117 | 
| child 61135 | 8f7d802b7a71 | 
| permissions | -rwxr-xr-x | 
| 48972 | 1  | 
#!/usr/bin/env bash  | 
2  | 
#  | 
|
3  | 
# Author: Makarius  | 
|
4  | 
#  | 
|
5  | 
# DESCRIPTION: build Isabelle documentation  | 
|
6  | 
||
7  | 
||
8  | 
## diagnostics  | 
|
9  | 
||
10  | 
PRG="$(basename "$0")"  | 
|
11  | 
||
12  | 
function usage()  | 
|
13  | 
{
 | 
|
14  | 
echo  | 
|
| 56429 | 15  | 
echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]"  | 
| 48972 | 16  | 
echo  | 
17  | 
echo " Options are:"  | 
|
| 56432 | 18  | 
echo " -a select all documentation sessions"  | 
| 48972 | 19  | 
echo " -j INT maximum number of parallel jobs (default 1)"  | 
| 
53208
 
bec95e287d26
prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
 
wenzelm 
parents: 
52740 
diff
changeset
 | 
20  | 
echo " -s system build mode"  | 
| 48972 | 21  | 
echo  | 
| 56432 | 22  | 
echo " Build Isabelle documentation from documentation sessions with"  | 
23  | 
echo " suitable document_variants entry."  | 
|
| 48972 | 24  | 
echo  | 
25  | 
exit 1  | 
|
26  | 
}  | 
|
27  | 
||
28  | 
function fail()  | 
|
29  | 
{
 | 
|
30  | 
echo "$1" >&2  | 
|
31  | 
exit 2  | 
|
32  | 
}  | 
|
33  | 
||
34  | 
function check_number()  | 
|
35  | 
{
 | 
|
36  | 
[ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""  | 
|
37  | 
}  | 
|
38  | 
||
39  | 
||
40  | 
## process command line  | 
|
41  | 
||
42  | 
ALL_DOCS="false"  | 
|
| 56429 | 43  | 
MAX_JOBS="1"  | 
44  | 
SYSTEM_MODE="false"  | 
|
| 48972 | 45  | 
|
| 
53208
 
bec95e287d26
prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
 
wenzelm 
parents: 
52740 
diff
changeset
 | 
46  | 
while getopts "aj:s" OPT  | 
| 48972 | 47  | 
do  | 
48  | 
case "$OPT" in  | 
|
49  | 
a)  | 
|
50  | 
ALL_DOCS="true"  | 
|
51  | 
;;  | 
|
52  | 
j)  | 
|
53  | 
check_number "$OPTARG"  | 
|
| 56429 | 54  | 
MAX_JOBS="$OPTARG"  | 
| 
53208
 
bec95e287d26
prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
 
wenzelm 
parents: 
52740 
diff
changeset
 | 
55  | 
;;  | 
| 
 
bec95e287d26
prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
 
wenzelm 
parents: 
52740 
diff
changeset
 | 
56  | 
s)  | 
| 56429 | 57  | 
SYSTEM_MODE="true"  | 
| 48972 | 58  | 
;;  | 
59  | 
\?)  | 
|
60  | 
usage  | 
|
61  | 
;;  | 
|
62  | 
esac  | 
|
63  | 
done  | 
|
64  | 
||
65  | 
shift $(($OPTIND - 1))  | 
|
66  | 
||
| 56429 | 67  | 
[ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage  | 
| 49131 | 68  | 
|
| 48972 | 69  | 
|
70  | 
## main  | 
|
71  | 
||
| 56429 | 72  | 
isabelle_admin_build jars || exit $?  | 
| 48972 | 73  | 
|
| 56429 | 74  | 
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"  | 
| 49131 | 75  | 
|
| 56429 | 76  | 
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \
 | 
77  | 
"$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@"  | 
|
| 
49005
 
96d5e42e5e3a
approximative build of pdf documents in 1 pass instead of 3;
 
wenzelm 
parents: 
49002 
diff
changeset
 | 
78  |