| author | blanchet | 
| Mon, 07 Aug 2017 10:59:49 +0200 | |
| changeset 66362 | 9b70e98490da | 
| parent 62589 | b5783412bfed | 
| child 67173 | e746db6db903 | 
| 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  | 
| 
62589
 
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
 
wenzelm 
parents: 
52748 
diff
changeset
 | 
131  | 
isabelle latex -o sty "$ROOT_NAME.tex" && \  | 
| 
 
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
 
wenzelm 
parents: 
52748 
diff
changeset
 | 
132  | 
isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \  | 
| 
 
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
 
wenzelm 
parents: 
52748 
diff
changeset
 | 
133  | 
    { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
 | 
| 
 
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
 
wenzelm 
parents: 
52748 
diff
changeset
 | 
134  | 
    { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
 | 
| 
 
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
 
wenzelm 
parents: 
52748 
diff
changeset
 | 
135  | 
isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \  | 
| 
 
b5783412bfed
prefer plain "isabelle" from PATH within Isabelle settings environment;
 
wenzelm 
parents: 
52748 
diff
changeset
 | 
136  | 
isabelle 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"  |