lib/Tools/latex
author wenzelm
Sat Oct 09 23:16:59 1999 +0200 (1999-10-09)
changeset 7815 cd0fe98db185
parent 7794 37069d910cbe
child 7857 a49a3978fe3a
permissions -rwxr-xr-x
support bibtex;
tuned;
wenzelm@7772
     1
#!/bin/bash
wenzelm@7772
     2
#
wenzelm@7772
     3
# $Id$
wenzelm@7772
     4
#
wenzelm@7794
     5
# DESCRIPTION: run LaTeX (and related tools)
wenzelm@7772
     6
wenzelm@7772
     7
wenzelm@7772
     8
PRG=$(basename $0)
wenzelm@7772
     9
wenzelm@7772
    10
function usage()
wenzelm@7772
    11
{
wenzelm@7772
    12
  echo
wenzelm@7794
    13
  echo "Usage: $PRG [OPTIONS] [FILE]"
wenzelm@7772
    14
  echo
wenzelm@7772
    15
  echo "  Options are:"
wenzelm@7815
    16
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
wenzelm@7815
    17
  echo "                 pdf, or bbl"
wenzelm@7772
    18
  echo
wenzelm@7772
    19
  echo
wenzelm@7794
    20
  echo "  Run LaTeX (and related tools) on FILE (default root.tex), producing the"
wenzelm@7794
    21
  echo "  speficied output format."
wenzelm@7772
    22
  echo
wenzelm@7772
    23
  exit 1
wenzelm@7772
    24
}
wenzelm@7772
    25
wenzelm@7772
    26
function fail()
wenzelm@7772
    27
{
wenzelm@7772
    28
  echo "$1" >&2
wenzelm@7772
    29
  exit 2
wenzelm@7772
    30
}
wenzelm@7772
    31
wenzelm@7772
    32
wenzelm@7772
    33
## process command line
wenzelm@7772
    34
wenzelm@7772
    35
# options
wenzelm@7772
    36
wenzelm@7772
    37
OUTFORMAT=dvi
wenzelm@7772
    38
wenzelm@7772
    39
while getopts "o:" OPT
wenzelm@7772
    40
do
wenzelm@7772
    41
  case "$OPT" in
wenzelm@7772
    42
    o)
wenzelm@7772
    43
      OUTFORMAT="$OPTARG"
wenzelm@7772
    44
      ;;
wenzelm@7772
    45
    \?)
wenzelm@7772
    46
      usage
wenzelm@7772
    47
      ;;
wenzelm@7772
    48
  esac
wenzelm@7772
    49
done
wenzelm@7772
    50
wenzelm@7772
    51
shift $(($OPTIND - 1))
wenzelm@7772
    52
wenzelm@7772
    53
wenzelm@7772
    54
# args
wenzelm@7772
    55
wenzelm@7794
    56
FILE="root.tex"
wenzelm@7772
    57
[ $# -ge 1 ] && { FILE="$1"; shift; }
wenzelm@7772
    58
wenzelm@7794
    59
[ $# -ne 0 ] && usage
wenzelm@7772
    60
wenzelm@7772
    61
wenzelm@7772
    62
## main
wenzelm@7772
    63
wenzelm@7815
    64
# check file
wenzelm@7815
    65
wenzelm@7772
    66
DIR=$(dirname "$FILE")
wenzelm@7777
    67
if [ "$DIR" = . ]; then
wenzelm@7772
    68
  FILEBASE=$(basename "$FILE" .tex)
wenzelm@7772
    69
else
wenzelm@7777
    70
  FILEBASE=$DIR/$(basename "$FILE" .tex)
wenzelm@7772
    71
fi
wenzelm@7772
    72
wenzelm@7794
    73
[ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"
wenzelm@7794
    74
wenzelm@7815
    75
wenzelm@7815
    76
# operations
wenzelm@7815
    77
wenzelm@7815
    78
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
wenzelm@7815
    79
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
wenzelm@7815
    80
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
wenzelm@7815
    81
function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
wenzelm@7815
    82
wenzelm@7815
    83
wenzelm@7815
    84
# process file
wenzelm@7815
    85
wenzelm@7772
    86
case "$OUTFORMAT" in
wenzelm@7772
    87
  dvi)
wenzelm@7815
    88
    run_latex
wenzelm@7794
    89
    RC=$?
wenzelm@7772
    90
    ;;
wenzelm@7772
    91
  dvi.gz)
wenzelm@7815
    92
    run_latex && \
wenzelm@7772
    93
    gzip -f "$FILEBASE.dvi"
wenzelm@7794
    94
    RC=$?
wenzelm@7772
    95
    ;;
wenzelm@7772
    96
  ps)
wenzelm@7815
    97
    run_latex && \
wenzelm@7815
    98
    run_dvips &&
wenzelm@7794
    99
    RC=$?
wenzelm@7772
   100
    ;;
wenzelm@7772
   101
  ps.gz)
wenzelm@7815
   102
    run_latex && \
wenzelm@7815
   103
    run_dvips &&
wenzelm@7772
   104
    gzip -f "$FILEBASE.ps"
wenzelm@7794
   105
    RC=$?
wenzelm@7772
   106
    ;;
wenzelm@7772
   107
  pdf)
wenzelm@7815
   108
    run_pdflatex
wenzelm@7815
   109
    RC=$?
wenzelm@7815
   110
    ;;
wenzelm@7815
   111
  bbl)
wenzelm@7815
   112
    run_bibtex
wenzelm@7794
   113
    RC=$?
wenzelm@7772
   114
    ;;
wenzelm@7772
   115
  *)
wenzelm@7772
   116
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7772
   117
    ;;
wenzelm@7772
   118
esac
wenzelm@7794
   119
wenzelm@7794
   120
exit $RC