| author | wenzelm | 
| Fri, 06 Nov 2020 13:43:49 +0100 | |
| changeset 72553 | 4e9d22dcd595 | 
| parent 72309 | 564012e31db1 | 
| child 73726 | aa7662e475b6 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1 | #!/usr/bin/env bash | 
| 7772 | 2 | # | 
| 9788 | 3 | # Author: Markus Wenzel, TU Muenchen | 
| 7772 | 4 | # | 
| 7794 | 5 | # DESCRIPTION: run LaTeX (and related tools) | 
| 7772 | 6 | |
| 7 | ||
| 10511 | 8 | PRG="$(basename "$0")" | 
| 7772 | 9 | |
| 10 | function usage() | |
| 11 | {
 | |
| 12 | echo | |
| 28650 | 13 | echo "Usage: isabelle $PRG [OPTIONS] [FILE]" | 
| 7772 | 14 | echo | 
| 15 | echo " Options are:" | |
| 72309 
564012e31db1
discontinued obsolete DVI document format and related settings/tools;
 wenzelm parents: 
72230diff
changeset | 16 | echo " -o FORMAT specify output format: pdf (default), bbl, idx, sty" | 
| 7772 | 17 | echo | 
| 7857 | 18 | echo " Run LaTeX (and related tools) on FILE (default root.tex)," | 
| 19 | echo " producing the specified output format." | |
| 7772 | 20 | echo | 
| 21 | exit 1 | |
| 22 | } | |
| 23 | ||
| 24 | function fail() | |
| 25 | {
 | |
| 26 | echo "$1" >&2 | |
| 27 | exit 2 | |
| 28 | } | |
| 29 | ||
| 30 | ||
| 31 | ## process command line | |
| 32 | ||
| 33 | # options | |
| 34 | ||
| 52746 | 35 | OUTFORMAT=pdf | 
| 7772 | 36 | |
| 37 | while getopts "o:" OPT | |
| 38 | do | |
| 39 | case "$OPT" in | |
| 40 | o) | |
| 41 | OUTFORMAT="$OPTARG" | |
| 42 | ;; | |
| 43 | \?) | |
| 44 | usage | |
| 45 | ;; | |
| 46 | esac | |
| 47 | done | |
| 48 | ||
| 49 | shift $(($OPTIND - 1)) | |
| 50 | ||
| 51 | ||
| 52 | # args | |
| 53 | ||
| 7794 | 54 | FILE="root.tex" | 
| 9788 | 55 | [ "$#" -ge 1 ] && { FILE="$1"; shift; }
 | 
| 7772 | 56 | |
| 9788 | 57 | [ "$#" -ne 0 ] && usage | 
| 7772 | 58 | |
| 59 | ||
| 60 | ## main | |
| 61 | ||
| 8564 | 62 | # root file | 
| 7815 | 63 | |
| 48515 | 64 | DIR="$(dirname "$FILE")" | 
| 65 | FILEBASE="$(basename "$FILE" .tex)" | |
| 9788 | 66 | [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" | 
| 7772 | 67 | |
| 8568 | 68 | function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
 | 
| 7794 | 69 | |
| 7815 | 70 | |
| 71 | # operations | |
| 72 | ||
| 73 | function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
 | |
| 72230 | 74 | function run_bibtex () {
 | 
| 75 | $ISABELLE_BIBTEX </dev/null "$FILEBASE" | |
| 76 | RC="$?" | |
| 77 |   if [ "$RC" -gt 0 -a -f "${FILEBASE}.blg" ]; then
 | |
| 78 |     perl -n -e 'if (m/^I (found no.*$)/) { print "bibtex $1\n"; }' "${FILEBASE}.blg" >&2
 | |
| 79 | fi | |
| 80 | return "$RC" | |
| 81 | } | |
| 14344 | 82 | function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
 | 
| 16064 | 83 | function copy_styles () | 
| 84 | {
 | |
| 16161 | 85 | for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty | 
| 86 | do | |
| 16874 | 87 | TARGET="$DIR"/$(basename "$STYLEFILE") | 
| 26576 | 88 | perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET" | 
| 16161 | 89 | done | 
| 16064 | 90 | } | 
| 7815 | 91 | |
| 7772 | 92 | case "$OUTFORMAT" in | 
| 52746 | 93 | pdf) | 
| 94 | check_root && \ | |
| 95 | run_pdflatex | |
| 96 | RC="$?" | |
| 97 | ;; | |
| 7815 | 98 | bbl) | 
| 8564 | 99 | check_root && \ | 
| 7815 | 100 | run_bibtex | 
| 9788 | 101 | RC="$?" | 
| 7772 | 102 | ;; | 
| 14344 | 103 | idx) | 
| 104 | check_root && \ | |
| 105 | run_makeindex | |
| 106 | RC="$?" | |
| 107 | ;; | |
| 8564 | 108 | sty) | 
| 12846 
0fce95478e19
copy_styles replaces overly conservative update_styles;
 wenzelm parents: 
11845diff
changeset | 109 | copy_styles | 
| 9788 | 110 | RC="$?" | 
| 8564 | 111 | ;; | 
| 7772 | 112 | *) | 
| 113 | fail "Bad output format '$OUTFORMAT'" | |
| 114 | ;; | |
| 115 | esac | |
| 7794 | 116 | |
| 9788 | 117 | exit "$RC" |