lib/Tools/document

if_splits and split_if_asm

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: prepare theory session document


PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [DIR]"
  echo
  echo "  Options are:"
  echo "    -c           cleanup -- be aggressive in removing old stuff"
  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 'document')"
  echo "  producing the specified output format."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

CLEAN=""
OUTFORMAT=dvi

while getopts "co:" OPT
do
  case "$OPT" in
    c)
      CLEAN=true
      ;;
    o)
      OUTFORMAT="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

DIR="document"
[ "$#" -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

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

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

  [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"

  if [ -f IsaMakefile ]; then
    "$ISATOOL" make "$OUTFORMAT"
    RC="$?"
  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

  [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"

  exit "$RC"
)
RC="$?"


# install

[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"

#beware!
[ -n "$CLEAN" ] && rm -rf "$DIR"

exit "$RC"