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