1#!/usr/bin/env bash 2# 3# Author: Markus Wenzel, TU Muenchen 4# 5# DESCRIPTION: run LaTeX (and related tools) 6 7 8PRG="$(basename "$0")" 9 10function usage() 11{ 12 echo 13 echo "Usage: isabelle $PRG [OPTIONS] [FILE]" 14 echo 15 echo " Options are:" 16 echo " -o FORMAT specify output format: pdf (default), dvi, bbl, idx, sty" 17 echo 18 echo " Run LaTeX (and related tools) on FILE (default root.tex)," 19 echo " producing the specified output format." 20 echo 21 exit 1 22} 23 24function fail() 25{ 26 echo "$1" >&2 27 exit 2 28} 29 30 31## process command line 32 33# options 34 35OUTFORMAT=pdf 36 37while getopts "o:" OPT 38do 39 case "$OPT" in 40 o) 41 OUTFORMAT="$OPTARG" 42 ;; 43 \?) 44 usage 45 ;; 46 esac 47done 48 49shift $(($OPTIND - 1)) 50 51 52# args 53 54FILE="root.tex" 55[ "$#" -ge 1 ] && { FILE="$1"; shift; } 56 57[ "$#" -ne 0 ] && usage 58 59 60## main 61 62# root file 63 64DIR="$(dirname "$FILE")" 65FILEBASE="$(basename "$FILE" .tex)" 66[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" 67 68function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } 69 70 71# operations 72 73function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } 74function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } 75function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } 76function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } 77function copy_styles () 78{ 79 for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty 80 do 81 TARGET="$DIR"/$(basename "$STYLEFILE") 82 perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET" 83 done 84} 85 86case "$OUTFORMAT" in 87 pdf) 88 check_root && \ 89 run_pdflatex 90 RC="$?" 91 ;; 92 dvi) 93 check_root && \ 94 run_latex 95 RC="$?" 96 ;; 97 bbl) 98 check_root && \ 99 run_bibtex 100 RC="$?" 101 ;; 102 idx) 103 check_root && \ 104 run_makeindex 105 RC="$?" 106 ;; 107 sty) 108 copy_styles 109 RC="$?" 110 ;; 111 *) 112 fail "Bad output format '$OUTFORMAT'" 113 ;; 114esac 115 116exit "$RC" 117