#!/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 *.ind *.idx *.ilg *.bbl *.blg *.log

  "$ISATOOL" latex -o sty && \

  "$ISATOOL" latex -o "$FMT" && \

  { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \

  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \

  "$ISATOOL" latex -o "$FMT"

}

(

  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

  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then

    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"

  fi

  exit "$RC"

)

RC="$?"

# install

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

#beware!

[ -n "$CLEAN" ] && rm -rf "$DIR"

exit "$RC"