wenzelm@7793: #!/bin/bash wenzelm@7793: # wenzelm@7793: # $Id$ wenzelm@7793: # wenzelm@7793: # DESCRIPTION: prepare theory session document wenzelm@7793: wenzelm@7793: wenzelm@7793: PRG=$(basename $0) wenzelm@7793: wenzelm@7793: function usage() wenzelm@7793: { wenzelm@7793: echo wenzelm@7793: echo "Usage: $PRG [OPTIONS] [DIR]" wenzelm@7793: echo wenzelm@7793: echo " Options are:" wenzelm@7793: echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf" wenzelm@7793: echo wenzelm@7793: echo wenzelm@7793: echo " Prepare the theory session document in DIR (default .)" wenzelm@7793: echo " producing the speficied output format." wenzelm@7793: echo wenzelm@7793: exit 1 wenzelm@7793: } wenzelm@7793: wenzelm@7793: function fail() wenzelm@7793: { wenzelm@7793: echo "$1" >&2 wenzelm@7793: exit 2 wenzelm@7793: } wenzelm@7793: wenzelm@7793: wenzelm@7793: ## process command line wenzelm@7793: wenzelm@7793: # options wenzelm@7793: wenzelm@7793: OUTFORMAT=dvi wenzelm@7793: wenzelm@7793: while getopts "o:" OPT wenzelm@7793: do wenzelm@7793: case "$OPT" in wenzelm@7793: o) wenzelm@7793: OUTFORMAT="$OPTARG" wenzelm@7793: ;; wenzelm@7793: \?) wenzelm@7793: usage wenzelm@7793: ;; wenzelm@7793: esac wenzelm@7793: done wenzelm@7793: wenzelm@7793: shift $(($OPTIND - 1)) wenzelm@7793: wenzelm@7793: wenzelm@7793: # args wenzelm@7793: wenzelm@7793: DIR="." wenzelm@7793: [ $# -ge 1 ] && { DIR="$1"; shift; } wenzelm@7793: wenzelm@7793: [ $# -ne 0 ] && usage wenzelm@7793: wenzelm@7793: wenzelm@7793: ## main wenzelm@7793: wenzelm@7814: # check format wenzelm@7814: wenzelm@7814: case "$OUTFORMAT" in wenzelm@7814: dvi | dvi.gz | ps | ps.gz | pdf) wenzelm@7814: ;; wenzelm@7814: *) wenzelm@7814: fail "Bad output format '$OUTFORMAT'" wenzelm@7814: ;; wenzelm@7814: esac wenzelm@7814: wenzelm@7814: wenzelm@7814: # prepare document wenzelm@7793: wenzelm@7793: cd "$DIR" || fail "Bad directory '$DIR'" wenzelm@7793: wenzelm@7814: function pre_latex () wenzelm@7814: { wenzelm@7814: local FMT="$1" wenzelm@7814: if [ -f root.bib ] wenzelm@7814: then wenzelm@7814: $ISATOOL latex -o "$FMT" && \ wenzelm@7814: $ISATOOL latex -o bbl && \ wenzelm@7814: $ISATOOL latex -o "$FMT" wenzelm@7814: else wenzelm@7814: $ISATOOL latex -o "$FMT" wenzelm@7814: fi wenzelm@7814: } wenzelm@7814: wenzelm@7793: if [ -f IsaMakefile ]; then wenzelm@7793: $ISATOOL make "$OUTFORMAT" wenzelm@7793: RC=$? #FIXME !?? wenzelm@7793: elif [ "$OUTFORMAT" = pdf ]; then wenzelm@7814: pre_latex pdf && \ wenzelm@7814: $ISATOOL latex -o pdf wenzelm@7793: RC=$? wenzelm@7793: else wenzelm@7814: pre_latex dvi && \ wenzelm@7814: $ISATOOL latex -o "$OUTFORMAT" wenzelm@7793: RC=$? wenzelm@7793: fi wenzelm@7793: wenzelm@7793: wenzelm@7814: # install wenzelm@7793: wenzelm@7793: [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'" wenzelm@7793: cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"