changeset 26576 | fc76b7b79ba9 |
parent 16874 | 3057990d20e0 |
child 26908 | 25fb7241f32e |
26575:042617a1c86c | 26576:fc76b7b79ba9 |
---|---|
70 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
70 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } |
71 |
71 |
72 |
72 |
73 # operations |
73 # operations |
74 |
74 |
75 #set by configure |
|
76 AUTO_PERL=perl |
|
77 |
|
78 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
75 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
79 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
76 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
80 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
77 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
81 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } |
78 function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } |
82 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
79 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
84 function copy_styles () |
81 function copy_styles () |
85 { |
82 { |
86 for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty |
83 for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty |
87 do |
84 do |
88 TARGET="$DIR"/$(basename "$STYLEFILE") |
85 TARGET="$DIR"/$(basename "$STYLEFILE") |
89 "$AUTO_PERL" -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET" |
86 perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET" |
90 done |
87 done |
91 } |
88 } |
92 |
89 |
93 function extract_syms () |
90 function extract_syms () |
94 { |
91 { |
95 "$AUTO_PERL" -n \ |
92 perl -n \ |
96 -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";' \ |
97 "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst" |
94 "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst" |
98 "$AUTO_PERL" -n \ |
95 perl -n \ |
99 -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \ |
96 -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \ |
100 "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst" |
97 "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst" |
101 } |
98 } |
102 |
99 |
103 case "$OUTFORMAT" in |
100 case "$OUTFORMAT" in |