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