lib/Tools/latex

obsolete (see 5a3a2a52648d);

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: run LaTeX (and related tools)


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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
  echo
  echo "  Options are:"
  echo "    -o FORMAT    specify output format: pdf (default), bbl, idx"
  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=pdf

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_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
function run_bibtex () {
  $ISABELLE_BIBTEX </dev/null "$FILEBASE"
  RC="$?"
  if [ "$RC" -gt 0 -a -f "${FILEBASE}.blg" ]; then
    perl -n -e 'if (m/^I (found no.*$)/) { print "bibtex $1\n"; }' "${FILEBASE}.blg" >&2
  fi
  return "$RC"
}
function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }

case "$OUTFORMAT" in
  pdf)
    check_root && \
    run_pdflatex
    RC="$?"
    ;;
  bbl)
    check_root && \
    run_bibtex
    RC="$?"
    ;;
  idx)
    check_root && \
    run_makeindex
    RC="$?"
    ;;
  *)
    fail "Bad output format '$OUTFORMAT'"
    ;;
esac

exit "$RC"