10 PRG="$(basename "$0")" |
10 PRG="$(basename "$0")" |
11 |
11 |
12 function usage() |
12 function usage() |
13 { |
13 { |
14 echo |
14 echo |
15 echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]" |
15 echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]" |
16 echo |
16 echo |
17 echo " Options are:" |
17 echo " Options are:" |
18 echo " -a select all doc sessions" |
18 echo " -a select all doc sessions" |
19 echo " -j INT maximum number of parallel jobs (default 1)" |
19 echo " -j INT maximum number of parallel jobs (default 1)" |
20 echo " -s system build mode" |
20 echo " -s system build mode" |
21 echo |
21 echo |
22 echo " Build Isabelle documentation from (doc) sessions." |
22 echo " Build Isabelle documentation from doc sessions with suitable" |
|
23 echo " document_variants." |
23 echo |
24 echo |
24 exit 1 |
25 exit 1 |
25 } |
26 } |
26 |
27 |
27 function fail() |
28 function fail() |
36 } |
37 } |
37 |
38 |
38 |
39 |
39 ## process command line |
40 ## process command line |
40 |
41 |
41 declare -a BUILD_ARGS=() |
|
42 |
|
43 |
|
44 # options |
|
45 |
|
46 ALL_DOCS="false" |
42 ALL_DOCS="false" |
|
43 MAX_JOBS="1" |
|
44 SYSTEM_MODE="false" |
47 |
45 |
48 while getopts "aj:s" OPT |
46 while getopts "aj:s" OPT |
49 do |
47 do |
50 case "$OPT" in |
48 case "$OPT" in |
51 a) |
49 a) |
52 ALL_DOCS="true" |
50 ALL_DOCS="true" |
53 ;; |
51 ;; |
54 j) |
52 j) |
55 check_number "$OPTARG" |
53 check_number "$OPTARG" |
56 BUILD_ARGS["${#BUILD_ARGS[@]}"]="-j" |
54 MAX_JOBS="$OPTARG" |
57 BUILD_ARGS["${#BUILD_ARGS[@]}"]="$OPTARG" |
|
58 ;; |
55 ;; |
59 s) |
56 s) |
60 BUILD_ARGS["${#BUILD_ARGS[@]}"]="-s" |
57 SYSTEM_MODE="true" |
61 ;; |
58 ;; |
62 \?) |
59 \?) |
63 usage |
60 usage |
64 ;; |
61 ;; |
65 esac |
62 esac |
66 done |
63 done |
67 |
64 |
68 shift $(($OPTIND - 1)) |
65 shift $(($OPTIND - 1)) |
69 |
66 |
70 |
67 [ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage |
71 # arguments |
|
72 |
|
73 if [ "$ALL_DOCS" = true ]; then |
|
74 BUILD_ARGS["${#BUILD_ARGS[@]}"]="-g" |
|
75 BUILD_ARGS["${#BUILD_ARGS[@]}"]="doc" |
|
76 else |
|
77 [ "$#" -eq 0 ] && usage |
|
78 fi |
|
79 |
|
80 BUILD_ARGS["${#BUILD_ARGS[@]}"]="--" |
|
81 |
|
82 while [ "$#" -ne 0 ]; do |
|
83 BUILD_ARGS["${#BUILD_ARGS[@]}"]="$1" |
|
84 shift |
|
85 done |
|
86 |
68 |
87 |
69 |
88 ## main |
70 ## main |
89 |
71 |
90 OUTPUT="$ISABELLE_TMP_PREFIX$$" |
72 isabelle_admin_build jars || exit $? |
91 mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\"" |
|
92 |
73 |
93 "$ISABELLE_TOOL" build -R -b "${BUILD_ARGS[@]}" |
74 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" |
94 RC=$? |
|
95 |
75 |
96 if [ "$RC" = 0 ]; then |
76 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \ |
97 "$ISABELLE_TOOL" build -o browser_info=false -o "document=pdf" \ |
77 "$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@" |
98 -o "document_output=$OUTPUT" -c "${BUILD_ARGS[@]}" |
|
99 RC=$? |
|
100 fi |
|
101 |
78 |
102 if [ "$RC" = 0 ]; then |
|
103 cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc" |
|
104 fi |
|
105 |
|
106 rm -rf "$OUTPUT" |
|
107 |
|
108 exit $RC |
|