#!/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, png, 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

 #set by configure

 AUTO_PERL=perl

 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 run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }

 function copy_styles ()

 {

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

   do

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

     rm -f $TARGET

     "$AUTO_PERL" -n -e 's/\$Id$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET

   done

 }

 function extract_syms ()

 {

   "$AUTO_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"

   "$AUTO_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="$?"

     ;;

   png)

     check_root && \

     run_thumbpdf

     RC="$?"

     ;;

   sty)

     copy_styles

     RC="$?"

     ;;

   syms)

     extract_syms

     RC="$?"

     ;;

   *)

     fail "Bad output format '$OUTFORMAT'"

     ;;

 esac

 exit "$RC"