equal
deleted
inserted
replaced
16 echo |
16 echo |
17 echo " Options are:" |
17 echo " Options are:" |
18 echo " -a all sessions" |
18 echo " -a all sessions" |
19 echo " -b build target images" |
19 echo " -b build target images" |
20 echo " -d DIR additional session directory with ROOT file" |
20 echo " -d DIR additional session directory with ROOT file" |
|
21 echo " -j INT maximum number of jobs (default 1)" |
21 echo " -l list sessions only" |
22 echo " -l list sessions only" |
22 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" |
23 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" |
|
24 echo " -v verbose" |
23 echo |
25 echo |
24 echo " Build and manage Isabelle sessions, depending on implicit" |
26 echo " Build and manage Isabelle sessions, depending on implicit" |
25 echo " ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" |
27 echo " ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" |
26 echo |
28 echo |
27 echo " ML_PLATFORM=\"$ML_PLATFORM\"" |
29 echo " ML_PLATFORM=\"$ML_PLATFORM\"" |
36 { |
38 { |
37 echo "$1" >&2 |
39 echo "$1" >&2 |
38 exit 2 |
40 exit 2 |
39 } |
41 } |
40 |
42 |
|
43 function check_number() |
|
44 { |
|
45 [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" |
|
46 } |
|
47 |
41 |
48 |
42 ## process command line |
49 ## process command line |
43 |
50 |
44 ALL_SESSIONS=false |
51 ALL_SESSIONS=false |
45 BUILD_IMAGES=false |
52 BUILD_IMAGES=false |
|
53 MAX_JOBS=1 |
46 LIST_ONLY=false |
54 LIST_ONLY=false |
|
55 VERBOSE=false |
47 |
56 |
48 declare -a MORE_DIRS=() |
57 declare -a MORE_DIRS=() |
49 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" |
58 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" |
50 |
59 |
51 while getopts "abd:lo:" OPT |
60 while getopts "abd:j:lo:v" OPT |
52 do |
61 do |
53 case "$OPT" in |
62 case "$OPT" in |
54 a) |
63 a) |
55 ALL_SESSIONS="true" |
64 ALL_SESSIONS="true" |
56 ;; |
65 ;; |
58 BUILD_IMAGES="true" |
67 BUILD_IMAGES="true" |
59 ;; |
68 ;; |
60 d) |
69 d) |
61 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG" |
70 MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG" |
62 ;; |
71 ;; |
|
72 j) |
|
73 check_number "$OPTARG" |
|
74 MAX_JOBS="$OPTARG" |
|
75 ;; |
63 l) |
76 l) |
64 LIST_ONLY="true" |
77 LIST_ONLY="true" |
65 ;; |
78 ;; |
66 o) |
79 o) |
67 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG" |
80 BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG" |
|
81 ;; |
|
82 v) |
|
83 VERBOSE="true" |
68 ;; |
84 ;; |
69 \?) |
85 \?) |
70 usage |
86 usage |
71 ;; |
87 ;; |
72 esac |
88 esac |
78 ## main |
94 ## main |
79 |
95 |
80 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } |
96 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } |
81 |
97 |
82 exec "$ISABELLE_TOOL" java isabelle.Build \ |
98 exec "$ISABELLE_TOOL" java isabelle.Build \ |
83 "$ALL_SESSIONS" "$BUILD_IMAGES" "$LIST_ONLY" \ |
99 "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \ |
84 "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" |
100 "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" |