#!/usr/bin/env bash

#

# $Id$

# Author: Markus Wenzel, TU Muenchen

#

# 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 "    -n NAME      specify document name (default 'document')"

  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"

  echo "    -t TAGS      specify tagged region markup"

  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=""

NAME="document"

OUTFORMAT=dvi

TAGS=""

while getopts "cn:o:t:" OPT

do

  case "$OPT" in

    c)

      CLEAN=true

      ;;

    n)

      NAME="$OPTARG"

      ;;

    o)

      OUTFORMAT="$OPTARG"

      ;;

    t)

      TAGS="$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

# tagged region markup

function prep_tags ()

{

  (

    IFS=","

    for TAG in $TAGS

    do

      case "$TAG" in

        /*)

  	  echo "\\isafoldtag{${TAG:1}}"

          ;;

        -*)

  	  echo "\\isadroptag{${TAG:1}}"

          ;;

        +*)

  	  echo "\\isakeeptag{${TAG:1}}"

          ;;

        *)

  	  echo "\\isakeeptag{${TAG}}"

          ;;

      esac

    done

  ) > isabelletags.sty

}

# 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 "../$NAME.$OUTFORMAT"

  prep_tags

  if [ -f IsaMakefile ]; then

    "$ISATOOL" make "$OUTFORMAT"

    RC="$?"

  elif [ "$OUTFORMAT" = pdf ]; then

    pre_latex pdf && \

    "$ISATOOL" latex -o pdf && \

    RC="$?"

  else

    pre_latex dvi && \

    "$ISATOOL" latex -o "$OUTFORMAT"

    RC="$?"

  fi

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

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

  fi

  exit "$RC"

)

RC="$?"

# install

[ "$RC" -ne 0 ] && fail "Document preparation failure in directory '$DIR'"

#beware!

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

exit "$RC"