#!/usr/bin/env bash

#

# $Id$

# Author: Markus Wenzel, TU Muenchen

#

# DESCRIPTION: run LaTeX (and related tools)

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

function usage()

{

  echo

  echo "Usage: $PRG [OPTIONS] [FILE]"

  echo

  echo "  Options are:"

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

  echo "                 pdf, bbl, idx, sty, syms"

  echo

  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"

  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

FILE="root.tex"

[ "$#" -ge 1 ] && { FILE="$1"; shift; }

[ "$#" -ne 0 ] && usage

## main

# root file

DIR=$(dirname "$FILE")

FILEBASE=$(basename "$FILE" .tex)

[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"

function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }

# operations

function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }

function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }

function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }

function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }

function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }

function copy_styles ()

{

  for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty

  do

    TARGET="$DIR"/$(basename "$STYLEFILE")

    perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"

  done

}

function extract_syms ()

{

  perl -n \

    -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \

    "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"

  perl -n \

    -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \

    "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"

}

case "$OUTFORMAT" in

  dvi)

    check_root && \

    run_latex

    RC="$?"

    ;;

  dvi.gz)

    check_root && \

    run_latex && \

    gzip -f "$FILEBASE.dvi"

    RC="$?"

    ;;

  ps)

    check_root && \

    run_latex && \

    run_dvips &&

    RC="$?"

    ;;

  ps.gz)

    check_root && \

    run_latex && \

    run_dvips &&

    gzip -f "$FILEBASE.ps"

    RC="$?"

    ;;

  pdf)

    check_root && \

    run_pdflatex

    RC="$?"

    ;;

  bbl)

    check_root && \

    run_bibtex

    RC="$?"

    ;;

  idx)

    check_root && \

    run_makeindex

    RC="$?"

    ;;

  sty)

    copy_styles

    RC="$?"

    ;;

  syms)

    extract_syms

    RC="$?"

    ;;

  *)

    fail "Bad output format '$OUTFORMAT'"

    ;;

esac

exit "$RC"