14 echo |
14 echo |
15 echo "Usage: $PRG [OPTIONS] [FILE]" |
15 echo "Usage: $PRG [OPTIONS] [FILE]" |
16 echo |
16 echo |
17 echo " Options are:" |
17 echo " Options are:" |
18 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," |
18 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," |
19 echo " pdf, bbl, png, sty" |
19 echo " pdf, bbl, png, sty, syms" |
20 echo |
20 echo |
21 echo " Run LaTeX (and related tools) on FILE (default root.tex)," |
21 echo " Run LaTeX (and related tools) on FILE (default root.tex)," |
22 echo " producing the specified output format." |
22 echo " producing the specified output format." |
23 echo |
23 echo |
24 exit 1 |
24 exit 1 |
71 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
71 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
72 |
72 |
73 |
73 |
74 # operations |
74 # operations |
75 |
75 |
|
76 #set by configure |
|
77 AUTO_PERL=perl |
|
78 |
76 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
79 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
77 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
80 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
78 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
81 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
79 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } |
82 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } |
80 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
83 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
81 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
84 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
82 function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; } |
85 function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; } |
|
86 |
|
87 function extract_syms () |
|
88 { |
|
89 "$AUTO_PERL" -n \ |
|
90 -e '!m,%requires, && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ |
|
91 "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst" |
|
92 "$AUTO_PERL" -n \ |
|
93 -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \ |
|
94 "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst" |
|
95 } |
83 |
96 |
84 case "$OUTFORMAT" in |
97 case "$OUTFORMAT" in |
85 dvi) |
98 dvi) |
86 check_root && \ |
99 check_root && \ |
87 run_latex |
100 run_latex |