| author | skalberg | 
| Tue, 21 Oct 2003 11:09:23 +0200 | |
| changeset 14242 | ec70653a02bf | 
| parent 12846 | 0fce95478e19 | 
| child 14344 | 0f0a2148a099 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1 | #!/usr/bin/env bash | 
| 7772 | 2 | # | 
| 3 | # $Id$ | |
| 9788 | 4 | # Author: Markus Wenzel, TU Muenchen | 
| 5 | # License: GPL (GNU GENERAL PUBLIC LICENSE) | |
| 7772 | 6 | # | 
| 7794 | 7 | # DESCRIPTION: run LaTeX (and related tools) | 
| 7772 | 8 | |
| 9 | ||
| 10511 | 10 | PRG="$(basename "$0")" | 
| 7772 | 11 | |
| 12 | function usage() | |
| 13 | {
 | |
| 14 | echo | |
| 7794 | 15 | echo "Usage: $PRG [OPTIONS] [FILE]" | 
| 7772 | 16 | echo | 
| 17 | echo " Options are:" | |
| 7815 | 18 | echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," | 
| 8564 | 19 | echo " pdf, bbl, png, sty" | 
| 7772 | 20 | echo | 
| 7857 | 21 | echo " Run LaTeX (and related tools) on FILE (default root.tex)," | 
| 22 | echo " producing the specified output format." | |
| 7772 | 23 | echo | 
| 24 | exit 1 | |
| 25 | } | |
| 26 | ||
| 27 | function fail() | |
| 28 | {
 | |
| 29 | echo "$1" >&2 | |
| 30 | exit 2 | |
| 31 | } | |
| 32 | ||
| 33 | ||
| 34 | ## process command line | |
| 35 | ||
| 36 | # options | |
| 37 | ||
| 38 | OUTFORMAT=dvi | |
| 39 | ||
| 40 | while getopts "o:" OPT | |
| 41 | do | |
| 42 | case "$OPT" in | |
| 43 | o) | |
| 44 | OUTFORMAT="$OPTARG" | |
| 45 | ;; | |
| 46 | \?) | |
| 47 | usage | |
| 48 | ;; | |
| 49 | esac | |
| 50 | done | |
| 51 | ||
| 52 | shift $(($OPTIND - 1)) | |
| 53 | ||
| 54 | ||
| 55 | # args | |
| 56 | ||
| 7794 | 57 | FILE="root.tex" | 
| 9788 | 58 | [ "$#" -ge 1 ] && { FILE="$1"; shift; }
 | 
| 7772 | 59 | |
| 9788 | 60 | [ "$#" -ne 0 ] && usage | 
| 7772 | 61 | |
| 62 | ||
| 63 | ## main | |
| 64 | ||
| 8564 | 65 | # root file | 
| 7815 | 66 | |
| 7772 | 67 | DIR=$(dirname "$FILE") | 
| 9788 | 68 | FILEBASE=$(basename "$FILE" .tex) | 
| 69 | [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" | |
| 7772 | 70 | |
| 8568 | 71 | function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
 | 
| 7794 | 72 | |
| 7815 | 73 | |
| 74 | # operations | |
| 75 | ||
| 76 | function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 | |
| 77 | function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 | |
| 78 | function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
 | |
| 11845 | 79 | function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 | 
| 7865 | 80 | function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
 | 
| 12846 
0fce95478e19
copy_styles replaces overly conservative update_styles;
 wenzelm parents: 
11845diff
changeset | 81 | function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
 | 
| 7815 | 82 | |
| 7772 | 83 | case "$OUTFORMAT" in | 
| 84 | dvi) | |
| 8564 | 85 | check_root && \ | 
| 7815 | 86 | run_latex | 
| 9788 | 87 | RC="$?" | 
| 7772 | 88 | ;; | 
| 89 | dvi.gz) | |
| 8564 | 90 | check_root && \ | 
| 7815 | 91 | run_latex && \ | 
| 7772 | 92 | gzip -f "$FILEBASE.dvi" | 
| 9788 | 93 | RC="$?" | 
| 7772 | 94 | ;; | 
| 95 | ps) | |
| 8564 | 96 | check_root && \ | 
| 7815 | 97 | run_latex && \ | 
| 98 | run_dvips && | |
| 9788 | 99 | RC="$?" | 
| 7772 | 100 | ;; | 
| 101 | ps.gz) | |
| 8564 | 102 | check_root && \ | 
| 7815 | 103 | run_latex && \ | 
| 104 | run_dvips && | |
| 7772 | 105 | gzip -f "$FILEBASE.ps" | 
| 9788 | 106 | RC="$?" | 
| 7772 | 107 | ;; | 
| 108 | pdf) | |
| 8564 | 109 | check_root && \ | 
| 7815 | 110 | run_pdflatex | 
| 9788 | 111 | RC="$?" | 
| 7815 | 112 | ;; | 
| 113 | bbl) | |
| 8564 | 114 | check_root && \ | 
| 7815 | 115 | run_bibtex | 
| 9788 | 116 | RC="$?" | 
| 7772 | 117 | ;; | 
| 7865 | 118 | png) | 
| 8564 | 119 | check_root && \ | 
| 7865 | 120 | run_thumbpdf | 
| 9788 | 121 | RC="$?" | 
| 7865 | 122 | ;; | 
| 8564 | 123 | sty) | 
| 12846 
0fce95478e19
copy_styles replaces overly conservative update_styles;
 wenzelm parents: 
11845diff
changeset | 124 | copy_styles | 
| 9788 | 125 | RC="$?" | 
| 8564 | 126 | ;; | 
| 7772 | 127 | *) | 
| 128 | fail "Bad output format '$OUTFORMAT'" | |
| 129 | ;; | |
| 130 | esac | |
| 7794 | 131 | |
| 9788 | 132 | exit "$RC" |