lib/Tools/latex
changeset 7772 c7b2f68c79fb
child 7777 ddbaf6785d0d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/latex	Thu Oct 07 12:27:44 1999 +0200
     1.3 @@ -0,0 +1,92 @@
     1.4 +#!/bin/bash
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +# DESCRIPTION: Isabelle wrapper for LaTeX (and friends)
     1.9 +
    1.10 +
    1.11 +PRG=$(basename $0)
    1.12 +
    1.13 +function usage()
    1.14 +{
    1.15 +  echo
    1.16 +  echo "Usage: $PRG [OPTIONS] FILE"
    1.17 +  echo
    1.18 +  echo "  Options are:"
    1.19 +  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
    1.20 +  echo
    1.21 +  echo
    1.22 +  echo "  Run LaTeX (and related tools) within the Isabelle environment."
    1.23 +  echo
    1.24 +  exit 1
    1.25 +}
    1.26 +
    1.27 +function fail()
    1.28 +{
    1.29 +  echo "$1" >&2
    1.30 +  exit 2
    1.31 +}
    1.32 +
    1.33 +
    1.34 +## process command line
    1.35 +
    1.36 +# options
    1.37 +
    1.38 +OUTFORMAT=dvi
    1.39 +
    1.40 +while getopts "o:" OPT
    1.41 +do
    1.42 +  case "$OPT" in
    1.43 +    o)
    1.44 +      OUTFORMAT="$OPTARG"
    1.45 +      ;;
    1.46 +    \?)
    1.47 +      usage
    1.48 +      ;;
    1.49 +  esac
    1.50 +done
    1.51 +
    1.52 +shift $(($OPTIND - 1))
    1.53 +
    1.54 +
    1.55 +# args
    1.56 +
    1.57 +FILE=""
    1.58 +[ $# -ge 1 ] && { FILE="$1"; shift; }
    1.59 +
    1.60 +[ $# -ne 0 -o -z "$FILE" ] && usage
    1.61 +
    1.62 +
    1.63 +## main
    1.64 +
    1.65 +DIR=$(dirname "$FILE")
    1.66 +if [ "$DIR" = "." ]; then
    1.67 +  FILEBASE=$(basename "$FILE" .tex)
    1.68 +else
    1.69 +  FILEBASE=$(dirname "$FILE")/$(basename "$FILE" .tex)
    1.70 +fi
    1.71 +
    1.72 +case "$OUTFORMAT" in
    1.73 +  dvi)
    1.74 +    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
    1.75 +    ;;
    1.76 +  dvi.gz)
    1.77 +    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
    1.78 +    gzip -f "$FILEBASE.dvi"
    1.79 +    ;;
    1.80 +  ps)
    1.81 +    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
    1.82 +    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"
    1.83 +    ;;
    1.84 +  ps.gz)
    1.85 +    $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"
    1.86 +    $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"
    1.87 +    gzip -f "$FILEBASE.ps"
    1.88 +    ;;
    1.89 +  pdf)
    1.90 +    $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"
    1.91 +    ;;
    1.92 +  *)
    1.93 +    fail "Bad output format '$OUTFORMAT'"
    1.94 +    ;;
    1.95 +esac