| author | haftmann | 
| Tue, 10 Oct 2006 09:17:20 +0200 | |
| changeset 20934 | 2b872c161747 | 
| parent 16874 | 3057990d20e0 | 
| child 26576 | fc76b7b79ba9 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1 | #!/usr/bin/env bash | 
| 7772 | 2 | # | 
| 3 | # $Id$ | |
| 9788 | 4 | # Author: Markus Wenzel, TU Muenchen | 
| 7772 | 5 | # | 
| 7794 | 6 | # DESCRIPTION: run LaTeX (and related tools) | 
| 7772 | 7 | |
| 8 | ||
| 10511 | 9 | PRG="$(basename "$0")" | 
| 7772 | 10 | |
| 11 | function usage() | |
| 12 | {
 | |
| 13 | echo | |
| 7794 | 14 | echo "Usage: $PRG [OPTIONS] [FILE]" | 
| 7772 | 15 | echo | 
| 16 | echo " Options are:" | |
| 7815 | 17 | echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," | 
| 14921 | 18 | echo " pdf, bbl, png, sty, syms" | 
| 7772 | 19 | echo | 
| 7857 | 20 | echo " Run LaTeX (and related tools) on FILE (default root.tex)," | 
| 21 | echo " producing the specified output format." | |
| 7772 | 22 | echo | 
| 23 | exit 1 | |
| 24 | } | |
| 25 | ||
| 26 | function fail() | |
| 27 | {
 | |
| 28 | echo "$1" >&2 | |
| 29 | exit 2 | |
| 30 | } | |
| 31 | ||
| 32 | ||
| 33 | ## process command line | |
| 34 | ||
| 35 | # options | |
| 36 | ||
| 37 | OUTFORMAT=dvi | |
| 38 | ||
| 39 | while getopts "o:" OPT | |
| 40 | do | |
| 41 | case "$OPT" in | |
| 42 | o) | |
| 43 | OUTFORMAT="$OPTARG" | |
| 44 | ;; | |
| 45 | \?) | |
| 46 | usage | |
| 47 | ;; | |
| 48 | esac | |
| 49 | done | |
| 50 | ||
| 51 | shift $(($OPTIND - 1)) | |
| 52 | ||
| 53 | ||
| 54 | # args | |
| 55 | ||
| 7794 | 56 | FILE="root.tex" | 
| 9788 | 57 | [ "$#" -ge 1 ] && { FILE="$1"; shift; }
 | 
| 7772 | 58 | |
| 9788 | 59 | [ "$#" -ne 0 ] && usage | 
| 7772 | 60 | |
| 61 | ||
| 62 | ## main | |
| 63 | ||
| 8564 | 64 | # root file | 
| 7815 | 65 | |
| 7772 | 66 | DIR=$(dirname "$FILE") | 
| 9788 | 67 | FILEBASE=$(basename "$FILE" .tex) | 
| 68 | [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" | |
| 7772 | 69 | |
| 8568 | 70 | function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
 | 
| 7794 | 71 | |
| 7815 | 72 | |
| 73 | # operations | |
| 74 | ||
| 14921 | 75 | #set by configure | 
| 15847 
c05c7670f166
restored AUTO_BASH/PERL -- beware of ./configure!
 wenzelm parents: 
15779diff
changeset | 76 | AUTO_PERL=perl | 
| 14921 | 77 | |
| 7815 | 78 | function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 | 
| 79 | function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 | |
| 80 | function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
 | |
| 14344 | 81 | function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
 | 
| 11845 | 82 | function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 | 
| 7865 | 83 | function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
 | 
| 16064 | 84 | function copy_styles () | 
| 85 | {
 | |
| 16161 | 86 | for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty | 
| 87 | do | |
| 16874 | 88 | TARGET="$DIR"/$(basename "$STYLEFILE") | 
| 89 | "$AUTO_PERL" -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET" | |
| 16161 | 90 | done | 
| 16064 | 91 | } | 
| 7815 | 92 | |
| 14921 | 93 | function extract_syms () | 
| 94 | {
 | |
| 95 | "$AUTO_PERL" -n \ | |
| 14970 
8159ade98144
more generous treatment of packages in draft prints;
 wenzelm parents: 
14921diff
changeset | 96 |     -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
 | 
| 14921 | 97 | "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst" | 
| 98 | "$AUTO_PERL" -n \ | |
| 99 |     -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
 | |
| 100 | "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst" | |
| 101 | } | |
| 102 | ||
| 7772 | 103 | case "$OUTFORMAT" in | 
| 104 | dvi) | |
| 8564 | 105 | check_root && \ | 
| 7815 | 106 | run_latex | 
| 9788 | 107 | RC="$?" | 
| 7772 | 108 | ;; | 
| 109 | dvi.gz) | |
| 8564 | 110 | check_root && \ | 
| 7815 | 111 | run_latex && \ | 
| 7772 | 112 | gzip -f "$FILEBASE.dvi" | 
| 9788 | 113 | RC="$?" | 
| 7772 | 114 | ;; | 
| 115 | ps) | |
| 8564 | 116 | check_root && \ | 
| 7815 | 117 | run_latex && \ | 
| 118 | run_dvips && | |
| 9788 | 119 | RC="$?" | 
| 7772 | 120 | ;; | 
| 121 | ps.gz) | |
| 8564 | 122 | check_root && \ | 
| 7815 | 123 | run_latex && \ | 
| 124 | run_dvips && | |
| 7772 | 125 | gzip -f "$FILEBASE.ps" | 
| 9788 | 126 | RC="$?" | 
| 7772 | 127 | ;; | 
| 128 | pdf) | |
| 8564 | 129 | check_root && \ | 
| 7815 | 130 | run_pdflatex | 
| 9788 | 131 | RC="$?" | 
| 7815 | 132 | ;; | 
| 133 | bbl) | |
| 8564 | 134 | check_root && \ | 
| 7815 | 135 | run_bibtex | 
| 9788 | 136 | RC="$?" | 
| 7772 | 137 | ;; | 
| 14344 | 138 | idx) | 
| 139 | check_root && \ | |
| 140 | run_makeindex | |
| 141 | RC="$?" | |
| 142 | ;; | |
| 7865 | 143 | png) | 
| 8564 | 144 | check_root && \ | 
| 7865 | 145 | run_thumbpdf | 
| 9788 | 146 | RC="$?" | 
| 7865 | 147 | ;; | 
| 8564 | 148 | sty) | 
| 12846 
0fce95478e19
copy_styles replaces overly conservative update_styles;
 wenzelm parents: 
11845diff
changeset | 149 | copy_styles | 
| 9788 | 150 | RC="$?" | 
| 8564 | 151 | ;; | 
| 14921 | 152 | syms) | 
| 153 | extract_syms | |
| 154 | RC="$?" | |
| 155 | ;; | |
| 7772 | 156 | *) | 
| 157 | fail "Bad output format '$OUTFORMAT'" | |
| 158 | ;; | |
| 159 | esac | |
| 7794 | 160 | |
| 9788 | 161 | exit "$RC" |