4 # Author: Markus Wenzel, TU Muenchen
6 # DESCRIPTION: run LaTeX (and related tools)
14 echo "Usage: $PRG [OPTIONS] [FILE]"
17 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz,"
18 echo " pdf, bbl, png, sty, syms"
20 echo " Run LaTeX (and related tools) on FILE (default root.tex),"
21 echo " producing the specified output format."
33 ## process command line
39 while getopts "o:" OPT
51 shift $(($OPTIND - 1))
57 [ "$#" -ge 1 ] && { FILE="$1"; shift; }
59 [ "$#" -ne 0 ] && usage
66 DIR=$(dirname "$FILE")
67 FILEBASE=$(basename "$FILE" .tex)
68 [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
70 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
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"; }
81 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
82 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
83 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
84 function copy_styles ()
86 for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
88 TARGET="$DIR"/$(basename $STYLEFILE)
90 "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g; print;' "$STYLEFILE" > "$TARGET"
91 #~ "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET
92 # the [I] is there to prevent CVS from expanding $Id...$ itself ;-)
96 function extract_syms ()
99 -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
100 "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
102 -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
103 "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
115 gzip -f "$FILEBASE.dvi"
128 gzip -f "$FILEBASE.ps"
160 fail "Bad output format '$OUTFORMAT'"