117 |
117 |
118 function pre_latex () |
118 function pre_latex () |
119 { |
119 { |
120 local FMT="$1" |
120 local FMT="$1" |
121 [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log |
121 [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log |
122 "$ISATOOL" latex -o sty && \ |
122 "$ISABELLE_TOOL" latex -o sty && \ |
123 "$ISATOOL" latex -o "$FMT" && \ |
123 "$ISABELLE_TOOL" latex -o "$FMT" && \ |
124 { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \ |
124 { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \ |
125 { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \ |
125 { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \ |
126 "$ISATOOL" latex -o "$FMT" |
126 "$ISABELLE_TOOL" latex -o "$FMT" |
127 } |
127 } |
128 |
128 |
129 ( |
129 ( |
130 cd "$DIR" || fail "Bad directory '$DIR'" |
130 cd "$DIR" || fail "Bad directory '$DIR'" |
131 |
131 |
132 [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" |
132 [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" |
133 |
133 |
134 prep_tags |
134 prep_tags |
135 |
135 |
136 if [ -f IsaMakefile ]; then |
136 if [ -f IsaMakefile ]; then |
137 "$ISATOOL" make "$OUTFORMAT" |
137 "$ISABELLE_TOOL" make "$OUTFORMAT" |
138 RC="$?" |
138 RC="$?" |
139 elif [ "$OUTFORMAT" = pdf ]; then |
139 elif [ "$OUTFORMAT" = pdf ]; then |
140 pre_latex pdf && \ |
140 pre_latex pdf && \ |
141 "$ISATOOL" latex -o pdf |
141 "$ISABELLE_TOOL" latex -o pdf |
142 RC="$?" |
142 RC="$?" |
143 else |
143 else |
144 pre_latex dvi && \ |
144 pre_latex dvi && \ |
145 "$ISATOOL" latex -o "$OUTFORMAT" |
145 "$ISABELLE_TOOL" latex -o "$OUTFORMAT" |
146 RC="$?" |
146 RC="$?" |
147 fi |
147 fi |
148 |
148 |
149 if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then |
149 if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then |
150 cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT" |
150 cp -f "root.$OUTFORMAT" "../$NAME.$OUTFORMAT" |