equal
deleted
inserted
replaced
12 echo |
12 echo |
13 echo "Usage: $PRG [OPTIONS] [FILE]" |
13 echo "Usage: $PRG [OPTIONS] [FILE]" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
16 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," |
16 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," |
17 echo " pdf, or bbl" |
17 echo " pdf, bbl, png" |
18 echo |
18 echo |
19 echo " Run LaTeX (and related tools) on FILE (default root.tex)," |
19 echo " Run LaTeX (and related tools) on FILE (default root.tex)," |
20 echo " producing the specified output format." |
20 echo " producing the specified output format." |
21 echo |
21 echo |
22 exit 1 |
22 exit 1 |
76 |
76 |
77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
77 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
78 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
78 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
79 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
79 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
80 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
80 function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
|
81 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
81 |
82 |
82 |
83 |
83 # process file |
84 # process file |
84 |
85 |
85 case "$OUTFORMAT" in |
86 case "$OUTFORMAT" in |
109 ;; |
110 ;; |
110 bbl) |
111 bbl) |
111 run_bibtex |
112 run_bibtex |
112 RC=$? |
113 RC=$? |
113 ;; |
114 ;; |
|
115 png) |
|
116 run_thumbpdf |
|
117 RC=$? |
|
118 ;; |
114 *) |
119 *) |
115 fail "Bad output format '$OUTFORMAT'" |
120 fail "Bad output format '$OUTFORMAT'" |
116 ;; |
121 ;; |
117 esac |
122 esac |
118 |
123 |