# HG changeset patch # User wenzelm # Date 939387807 -7200 # Node ID 37069d910cbe1be103ca82c48612439a01a97bed # Parent e0676a93234833c9ad9121339ec79c68e64bf01f pass RC; diff -r e0676a932348 -r 37069d910cbe lib/Tools/latex --- a/lib/Tools/latex Fri Oct 08 15:03:11 1999 +0200 +++ b/lib/Tools/latex Fri Oct 08 15:03:27 1999 +0200 @@ -2,7 +2,7 @@ # # $Id$ # -# DESCRIPTION: Isabelle wrapper for LaTeX (and friends) +# DESCRIPTION: run LaTeX (and related tools) PRG=$(basename $0) @@ -10,13 +10,14 @@ function usage() { echo - echo "Usage: $PRG [OPTIONS] FILE" + echo "Usage: $PRG [OPTIONS] [FILE]" echo echo " Options are:" echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf" echo echo - echo " Run LaTeX (and related tools) within the Isabelle environment." + echo " Run LaTeX (and related tools) on FILE (default root.tex), producing the" + echo " speficied output format." echo exit 1 } @@ -51,10 +52,10 @@ # args -FILE="" +FILE="root.tex" [ $# -ge 1 ] && { FILE="$1"; shift; } -[ $# -ne 0 -o -z "$FILE" ] && usage +[ $# -ne 0 ] && usage ## main @@ -66,27 +67,36 @@ FILEBASE=$DIR/$(basename "$FILE" .tex) fi +[ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" + case "$OUTFORMAT" in dvi) $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" + RC=$? ;; dvi.gz) - $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" + $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" && \ gzip -f "$FILEBASE.dvi" + RC=$? ;; ps) - $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" + $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" && \ $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi" + RC=$? ;; ps.gz) - $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" - $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi" + $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}" && \ + $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi" && \ gzip -f "$FILEBASE.ps" + RC=$? ;; pdf) $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}" + RC=$? ;; *) fail "Bad output format '$OUTFORMAT'" ;; esac + +exit $RC