lib/Tools/latex
author wenzelm
Fri, 01 Sep 2000 17:50:36 +0200
changeset 9788 df671fa2562a
parent 8568 b18540435f26
child 10511 efb3428c9879
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
wenzelm@7772
     1
#!/bin/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@9788
    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"; }
wenzelm@7815
    79
function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
wenzelm@7865
    80
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
wenzelm@7815
    81
wenzelm@8564
    82
function update_styles ()
wenzelm@8564
    83
{
wenzelm@9788
    84
  for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty
wenzelm@8564
    85
  do
wenzelm@8565
    86
    DEST="$DIR"/$(basename "$NAME")
wenzelm@8565
    87
    if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
wenzelm@8565
    88
      echo "updating $DEST"
wenzelm@8565
    89
      cp -f "$NAME" "$DEST"
wenzelm@8564
    90
    fi
wenzelm@8564
    91
  done
wenzelm@8564
    92
}
wenzelm@7815
    93
wenzelm@7772
    94
case "$OUTFORMAT" in
wenzelm@7772
    95
  dvi)
wenzelm@8564
    96
    check_root && \
wenzelm@7815
    97
    run_latex
wenzelm@9788
    98
    RC="$?"
wenzelm@7772
    99
    ;;
wenzelm@7772
   100
  dvi.gz)
wenzelm@8564
   101
    check_root && \
wenzelm@7815
   102
    run_latex && \
wenzelm@7772
   103
    gzip -f "$FILEBASE.dvi"
wenzelm@9788
   104
    RC="$?"
wenzelm@7772
   105
    ;;
wenzelm@7772
   106
  ps)
wenzelm@8564
   107
    check_root && \
wenzelm@7815
   108
    run_latex && \
wenzelm@7815
   109
    run_dvips &&
wenzelm@9788
   110
    RC="$?"
wenzelm@7772
   111
    ;;
wenzelm@7772
   112
  ps.gz)
wenzelm@8564
   113
    check_root && \
wenzelm@7815
   114
    run_latex && \
wenzelm@7815
   115
    run_dvips &&
wenzelm@7772
   116
    gzip -f "$FILEBASE.ps"
wenzelm@9788
   117
    RC="$?"
wenzelm@7772
   118
    ;;
wenzelm@7772
   119
  pdf)
wenzelm@8564
   120
    check_root && \
wenzelm@7815
   121
    run_pdflatex
wenzelm@9788
   122
    RC="$?"
wenzelm@7815
   123
    ;;
wenzelm@7815
   124
  bbl)
wenzelm@8564
   125
    check_root && \
wenzelm@7815
   126
    run_bibtex
wenzelm@9788
   127
    RC="$?"
wenzelm@7772
   128
    ;;
wenzelm@7865
   129
  png)
wenzelm@8564
   130
    check_root && \
wenzelm@7865
   131
    run_thumbpdf
wenzelm@9788
   132
    RC="$?"
wenzelm@7865
   133
    ;;
wenzelm@8564
   134
  sty)
wenzelm@8564
   135
    update_styles
wenzelm@9788
   136
    RC="$?"
wenzelm@8564
   137
    ;;
wenzelm@7772
   138
  *)
wenzelm@7772
   139
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7772
   140
    ;;
wenzelm@7772
   141
esac
wenzelm@7794
   142
wenzelm@9788
   143
exit "$RC"