#!/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 "    -v           be verbose"

   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

 VERBOSE=""

 while getopts "co:v" OPT

 do

   case "$OPT" in

     c)

       CLEAN=true

       ;;

     o)

       OUTFORMAT="$OPTARG"

       ;;

     v)

       VERBOSE=true

       ;;

     \?)

       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

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

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

     [ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2

   fi

   exit "$RC"

 )

 RC="$?"

 # install

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

 #beware!

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

 exit "$RC"