author | immler |
Wed, 12 Nov 2014 17:36:25 +0100 | |
changeset 58981 | 11b6c099f5f3 |
parent 52748 | 8e398d9bedf3 |
child 62589 | b5783412bfed |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
7793 | 2 |
# |
9788 | 3 |
# Author: Markus Wenzel, TU Muenchen |
7793 | 4 |
# |
5 |
# DESCRIPTION: prepare theory session document |
|
6 |
||
7 |
||
10511 | 8 |
PRG="$(basename "$0")" |
7793 | 9 |
|
10 |
function usage() |
|
11 |
{ |
|
12 |
echo |
|
28650 | 13 |
echo "Usage: isabelle $PRG [OPTIONS] [DIR]" |
7793 | 14 |
echo |
15 |
echo " Options are:" |
|
8654 | 16 |
echo " -c cleanup -- be aggressive in removing old stuff" |
17049 | 17 |
echo " -n NAME specify document name (default 'document')" |
52746 | 18 |
echo " -o FORMAT specify output format: pdf (default), dvi" |
17049 | 19 |
echo " -t TAGS specify tagged region markup" |
7793 | 20 |
echo |
8211 | 21 |
echo " Prepare the theory session document in DIR (default 'document')" |
7857 | 22 |
echo " producing the specified output format." |
7793 | 23 |
echo |
24 |
exit 1 |
|
25 |
} |
|
26 |
||
27 |
function fail() |
|
28 |
{ |
|
29 |
echo "$1" >&2 |
|
30 |
exit 2 |
|
31 |
} |
|
32 |
||
33 |
||
34 |
## process command line |
|
35 |
||
36 |
# options |
|
37 |
||
8211 | 38 |
CLEAN="" |
17049 | 39 |
NAME="document" |
52746 | 40 |
OUTFORMAT=pdf |
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
41 |
declare -a TAGS=() |
7793 | 42 |
|
17049 | 43 |
while getopts "cn:o:t:" OPT |
7793 | 44 |
do |
45 |
case "$OPT" in |
|
8211 | 46 |
c) |
47 |
CLEAN=true |
|
48 |
;; |
|
17049 | 49 |
n) |
50 |
NAME="$OPTARG" |
|
51 |
;; |
|
7793 | 52 |
o) |
53 |
OUTFORMAT="$OPTARG" |
|
54 |
;; |
|
17049 | 55 |
t) |
32390
468eff174a77
function splitarray: splightly more abstract version that accomodates older bashes;
wenzelm
parents:
32322
diff
changeset
|
56 |
splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}") |
17049 | 57 |
;; |
7793 | 58 |
\?) |
59 |
usage |
|
60 |
;; |
|
61 |
esac |
|
62 |
done |
|
63 |
||
64 |
shift $(($OPTIND - 1)) |
|
65 |
||
66 |
||
67 |
# args |
|
68 |
||
8211 | 69 |
DIR="document" |
9788 | 70 |
[ "$#" -ge 1 ] && { DIR="$1"; shift; } |
7793 | 71 |
|
9788 | 72 |
[ "$#" -ne 0 ] && usage |
7793 | 73 |
|
74 |
||
75 |
## main |
|
76 |
||
7814 | 77 |
# check format |
78 |
||
79 |
case "$OUTFORMAT" in |
|
52746 | 80 |
pdf | dvi) |
7814 | 81 |
;; |
82 |
*) |
|
83 |
fail "Bad output format '$OUTFORMAT'" |
|
84 |
;; |
|
85 |
esac |
|
86 |
||
87 |
||
48616
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
32390
diff
changeset
|
88 |
# document variants |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
32390
diff
changeset
|
89 |
|
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
32390
diff
changeset
|
90 |
ROOT_NAME="root_$NAME" |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
32390
diff
changeset
|
91 |
[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" |
17049 | 92 |
|
93 |
function prep_tags () |
|
94 |
{ |
|
95 |
( |
|
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
96 |
for TAG in "${TAGS[@]}" |
17049 | 97 |
do |
98 |
case "$TAG" in |
|
99 |
/*) |
|
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
100 |
echo "\\isafoldtag{${TAG:1}}" |
17049 | 101 |
;; |
102 |
-*) |
|
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
103 |
echo "\\isadroptag{${TAG:1}}" |
17049 | 104 |
;; |
105 |
+*) |
|
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
106 |
echo "\\isakeeptag{${TAG:1}}" |
17049 | 107 |
;; |
108 |
*) |
|
32322
45cb4a86eca2
change IFS only locally -- thanks to bash arrays;
wenzelm
parents:
29143
diff
changeset
|
109 |
echo "\\isakeeptag{${TAG}}" |
17049 | 110 |
;; |
111 |
esac |
|
112 |
done |
|
51822
7aebe43d6a14
avoid empty isabelletags.sty for the sake of arXiv;
wenzelm
parents:
51081
diff
changeset
|
113 |
echo |
17049 | 114 |
) > isabelletags.sty |
115 |
} |
|
116 |
||
117 |
||
7814 | 118 |
# prepare document |
7793 | 119 |
|
8211 | 120 |
( |
121 |
cd "$DIR" || fail "Bad directory '$DIR'" |
|
122 |
||
52748 | 123 |
[ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log |
17049 | 124 |
|
125 |
prep_tags |
|
8654 | 126 |
|
48657
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48637
diff
changeset
|
127 |
if [ -f build ]; then |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48637
diff
changeset
|
128 |
./build "$OUTFORMAT" "$NAME" |
9788 | 129 |
RC="$?" |
8211 | 130 |
else |
52747 | 131 |
"$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \ |
132 |
"$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ |
|
133 |
{ [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \ |
|
134 |
{ [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \ |
|
135 |
"$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ |
|
48616
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
32390
diff
changeset
|
136 |
"$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" |
9788 | 137 |
RC="$?" |
8211 | 138 |
fi |
139 |
||
48616
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
32390
diff
changeset
|
140 |
if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
32390
diff
changeset
|
141 |
cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT" |
11581 | 142 |
fi |
8211 | 143 |
|
8217 | 144 |
exit "$RC" |
8211 | 145 |
) |
9788 | 146 |
RC="$?" |
7793 | 147 |
|
148 |
||
7814 | 149 |
# install |
7793 | 150 |
|
17049 | 151 |
[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'" |
8211 | 152 |
|
153 |
#beware! |
|
154 |
[ -n "$CLEAN" ] && rm -rf "$DIR" |
|
155 |
||
156 |
exit "$RC" |