lib/Tools/latex
author kleing
Thu, 08 Jan 2004 04:32:52 +0100
changeset 14344 0f0a2148a099
parent 12846 0fce95478e19
child 14921 4ad751fa50c1
permissions -rwxr-xr-x
run makeindex if necessary
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@7772
     2
#
wenzelm@7772
     3
# $Id$
wenzelm@9788
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@9788
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@7772
     6
#
wenzelm@7794
     7
# DESCRIPTION: run LaTeX (and related tools)
wenzelm@7772
     8
wenzelm@7772
     9
wenzelm@10511
    10
PRG="$(basename "$0")"
wenzelm@7772
    11
wenzelm@7772
    12
function usage()
wenzelm@7772
    13
{
wenzelm@7772
    14
  echo
wenzelm@7794
    15
  echo "Usage: $PRG [OPTIONS] [FILE]"
wenzelm@7772
    16
  echo
wenzelm@7772
    17
  echo "  Options are:"
wenzelm@7815
    18
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
wenzelm@8564
    19
  echo "                 pdf, bbl, png, sty"
wenzelm@7772
    20
  echo
wenzelm@7857
    21
  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
wenzelm@7857
    22
  echo "  producing the specified output format."
wenzelm@7772
    23
  echo
wenzelm@7772
    24
  exit 1
wenzelm@7772
    25
}
wenzelm@7772
    26
wenzelm@7772
    27
function fail()
wenzelm@7772
    28
{
wenzelm@7772
    29
  echo "$1" >&2
wenzelm@7772
    30
  exit 2
wenzelm@7772
    31
}
wenzelm@7772
    32
wenzelm@7772
    33
wenzelm@7772
    34
## process command line
wenzelm@7772
    35
wenzelm@7772
    36
# options
wenzelm@7772
    37
wenzelm@7772
    38
OUTFORMAT=dvi
wenzelm@7772
    39
wenzelm@7772
    40
while getopts "o:" OPT
wenzelm@7772
    41
do
wenzelm@7772
    42
  case "$OPT" in
wenzelm@7772
    43
    o)
wenzelm@7772
    44
      OUTFORMAT="$OPTARG"
wenzelm@7772
    45
      ;;
wenzelm@7772
    46
    \?)
wenzelm@7772
    47
      usage
wenzelm@7772
    48
      ;;
wenzelm@7772
    49
  esac
wenzelm@7772
    50
done
wenzelm@7772
    51
wenzelm@7772
    52
shift $(($OPTIND - 1))
wenzelm@7772
    53
wenzelm@7772
    54
wenzelm@7772
    55
# args
wenzelm@7772
    56
wenzelm@7794
    57
FILE="root.tex"
wenzelm@9788
    58
[ "$#" -ge 1 ] && { FILE="$1"; shift; }
wenzelm@7772
    59
wenzelm@9788
    60
[ "$#" -ne 0 ] && usage
wenzelm@7772
    61
wenzelm@7772
    62
wenzelm@7772
    63
## main
wenzelm@7772
    64
wenzelm@8564
    65
# root file
wenzelm@7815
    66
wenzelm@7772
    67
DIR=$(dirname "$FILE")
wenzelm@9788
    68
FILEBASE=$(basename "$FILE" .tex)
wenzelm@9788
    69
[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
wenzelm@7772
    70
wenzelm@8568
    71
function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
wenzelm@7794
    72
wenzelm@7815
    73
wenzelm@7815
    74
# operations
wenzelm@7815
    75
wenzelm@7815
    76
function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
wenzelm@7815
    77
function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
wenzelm@7815
    78
function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
kleing@14344
    79
function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
wenzelm@11845
    80
function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
wenzelm@7865
    81
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
wenzelm@12846
    82
function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
wenzelm@7815
    83
wenzelm@7772
    84
case "$OUTFORMAT" in
wenzelm@7772
    85
  dvi)
wenzelm@8564
    86
    check_root && \
wenzelm@7815
    87
    run_latex
wenzelm@9788
    88
    RC="$?"
wenzelm@7772
    89
    ;;
wenzelm@7772
    90
  dvi.gz)
wenzelm@8564
    91
    check_root && \
wenzelm@7815
    92
    run_latex && \
wenzelm@7772
    93
    gzip -f "$FILEBASE.dvi"
wenzelm@9788
    94
    RC="$?"
wenzelm@7772
    95
    ;;
wenzelm@7772
    96
  ps)
wenzelm@8564
    97
    check_root && \
wenzelm@7815
    98
    run_latex && \
wenzelm@7815
    99
    run_dvips &&
wenzelm@9788
   100
    RC="$?"
wenzelm@7772
   101
    ;;
wenzelm@7772
   102
  ps.gz)
wenzelm@8564
   103
    check_root && \
wenzelm@7815
   104
    run_latex && \
wenzelm@7815
   105
    run_dvips &&
wenzelm@7772
   106
    gzip -f "$FILEBASE.ps"
wenzelm@9788
   107
    RC="$?"
wenzelm@7772
   108
    ;;
wenzelm@7772
   109
  pdf)
wenzelm@8564
   110
    check_root && \
wenzelm@7815
   111
    run_pdflatex
wenzelm@9788
   112
    RC="$?"
wenzelm@7815
   113
    ;;
wenzelm@7815
   114
  bbl)
wenzelm@8564
   115
    check_root && \
wenzelm@7815
   116
    run_bibtex
wenzelm@9788
   117
    RC="$?"
wenzelm@7772
   118
    ;;
kleing@14344
   119
  idx)
kleing@14344
   120
    check_root && \
kleing@14344
   121
    run_makeindex
kleing@14344
   122
    RC="$?"
kleing@14344
   123
    ;;
wenzelm@7865
   124
  png)
wenzelm@8564
   125
    check_root && \
wenzelm@7865
   126
    run_thumbpdf
wenzelm@9788
   127
    RC="$?"
wenzelm@7865
   128
    ;;
wenzelm@8564
   129
  sty)
wenzelm@12846
   130
    copy_styles
wenzelm@9788
   131
    RC="$?"
wenzelm@8564
   132
    ;;
wenzelm@7772
   133
  *)
wenzelm@7772
   134
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7772
   135
    ;;
wenzelm@7772
   136
esac
wenzelm@7794
   137
wenzelm@9788
   138
exit "$RC"