| changeset 16064 | 7953879aa6cf |
| parent 15847 | c05c7670f166 |
| child 16161 | 519d717ae9e3 |
| 16063:7dd4eb2c8055 | 16064:7953879aa6cf |
|---|---|
79 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
79 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
80 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
80 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
81 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } |
81 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } |
82 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
82 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
83 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
83 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
84 function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; } |
84 function copy_styles () |
85 { |
|
86 cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; |
|
87 "$AUTO_PERL" -n -i -e 's/\$Id(?::\s)*([^\$]*)\$/originating from CVS: $1/g; print;' "$DIR"/*.sty |
|
88 } |
|
85 |
89 |
86 function extract_syms () |
90 function extract_syms () |
87 { |
91 { |
88 "$AUTO_PERL" -n \ |
92 "$AUTO_PERL" -n \ |
89 -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ |
93 -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ |