lib/Tools/document

misc improvements;

#!/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,"
  echo "                 ps.gz, pdf"
  echo
  echo "  Prepare the theory session document in DIR (default '.')"
  echo "  producing the specified 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

# check format

case "$OUTFORMAT" in
  dvi | dvi.gz | ps | ps.gz | pdf)
    ;;
  *)
    fail "Bad output format '$OUTFORMAT'"
    ;;
esac


# prepare document

cd "$DIR" || fail "Bad directory '$DIR'"

function pre_latex ()
{
  local FMT="$1"
  rm -f *.aux
  if [ -f root.bib ]
  then
    $ISATOOL latex -o "$FMT" && \
    $ISATOOL latex -o bbl && \
    $ISATOOL latex -o "$FMT"
  else
    $ISATOOL latex -o "$FMT"
  fi
}

if [ -f IsaMakefile ]; then
  $ISATOOL make "$OUTFORMAT"
  RC=$?   #FIXME !??
elif [ "$OUTFORMAT" = pdf ]; then
  pre_latex pdf && \
  $ISATOOL latex -o pdf && \
  { if [ -n "$ISABELLE_THUMBPDF" ]; then
      $ISATOOL latex -o png && \
      $ISATOOL latex -o pdf
    fi; }
  RC=$?
else
  pre_latex 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"