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