lib/Tools/latex
author wenzelm
Thu Oct 07 12:27:44 1999 +0200 (1999-10-07)
changeset 7772 c7b2f68c79fb
child 7777 ddbaf6785d0d
permissions -rwxr-xr-x
Isabelle wrapper for LaTeX (and friends);
wenzelm@7772
     1
#!/bin/bash
wenzelm@7772
     2
#
wenzelm@7772
     3
# $Id$
wenzelm@7772
     4
#
wenzelm@7772
     5
# DESCRIPTION: Isabelle wrapper for LaTeX (and friends)
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@7772
    13
  echo "Usage: $PRG [OPTIONS] FILE"
wenzelm@7772
    14
  echo
wenzelm@7772
    15
  echo "  Options are:"
wenzelm@7772
    16
  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
wenzelm@7772
    17
  echo
wenzelm@7772
    18
  echo
wenzelm@7772
    19
  echo "  Run LaTeX (and related tools) within the Isabelle environment."
wenzelm@7772
    20
  echo
wenzelm@7772
    21
  exit 1
wenzelm@7772
    22
}
wenzelm@7772
    23
wenzelm@7772
    24
function fail()
wenzelm@7772
    25
{
wenzelm@7772
    26
  echo "$1" >&2
wenzelm@7772
    27
  exit 2
wenzelm@7772
    28
}
wenzelm@7772
    29
wenzelm@7772
    30
wenzelm@7772
    31
## process command line
wenzelm@7772
    32
wenzelm@7772
    33
# options
wenzelm@7772
    34
wenzelm@7772
    35
OUTFORMAT=dvi
wenzelm@7772
    36
wenzelm@7772
    37
while getopts "o:" OPT
wenzelm@7772
    38
do
wenzelm@7772
    39
  case "$OPT" in
wenzelm@7772
    40
    o)
wenzelm@7772
    41
      OUTFORMAT="$OPTARG"
wenzelm@7772
    42
      ;;
wenzelm@7772
    43
    \?)
wenzelm@7772
    44
      usage
wenzelm@7772
    45
      ;;
wenzelm@7772
    46
  esac
wenzelm@7772
    47
done
wenzelm@7772
    48
wenzelm@7772
    49
shift $(($OPTIND - 1))
wenzelm@7772
    50
wenzelm@7772
    51
wenzelm@7772
    52
# args
wenzelm@7772
    53
wenzelm@7772
    54
FILE=""
wenzelm@7772
    55
[ $# -ge 1 ] && { FILE="$1"; shift; }
wenzelm@7772
    56
wenzelm@7772
    57
[ $# -ne 0 -o -z "$FILE" ] && usage
wenzelm@7772
    58
wenzelm@7772
    59
wenzelm@7772
    60
## main
wenzelm@7772
    61
wenzelm@7772
    62
DIR=$(dirname "$FILE")
wenzelm@7772
    63
if [ "$DIR" = "." ]; then
wenzelm@7772
    64
  FILEBASE=$(basename "$FILE" .tex)
wenzelm@7772
    65
else
wenzelm@7772
    66
  FILEBASE=$(dirname "$FILE")/$(basename "$FILE" .tex)
wenzelm@7772
    67
fi
wenzelm@7772
    68
wenzelm@7772
    69
case "$OUTFORMAT" in
wenzelm@7772
    70
  dvi)
wenzelm@7772
    71
    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
wenzelm@7772
    72
    ;;
wenzelm@7772
    73
  dvi.gz)
wenzelm@7772
    74
    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
wenzelm@7772
    75
    gzip -f "$FILEBASE.dvi"
wenzelm@7772
    76
    ;;
wenzelm@7772
    77
  ps)
wenzelm@7772
    78
    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
wenzelm@7772
    79
    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"
wenzelm@7772
    80
    ;;
wenzelm@7772
    81
  ps.gz)
wenzelm@7772
    82
    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
wenzelm@7772
    83
    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"
wenzelm@7772
    84
    gzip -f "$FILEBASE.ps"
wenzelm@7772
    85
    ;;
wenzelm@7772
    86
  pdf)
wenzelm@7772
    87
    $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"
wenzelm@7772
    88
    ;;
wenzelm@7772
    89
  *)
wenzelm@7772
    90
    fail "Bad output format '$OUTFORMAT'"
wenzelm@7772
    91
    ;;
wenzelm@7772
    92
esac