equal
deleted
inserted
replaced
76 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
76 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
77 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
77 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } |
78 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
78 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } |
79 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
79 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } |
80 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
80 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } |
81 |
81 function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; } |
82 function update_styles () |
|
83 { |
|
84 for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty |
|
85 do |
|
86 DEST="$DIR"/$(basename "$NAME") |
|
87 if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then |
|
88 echo "updating $DEST" |
|
89 cp -f "$NAME" "$DEST" |
|
90 fi |
|
91 done |
|
92 } |
|
93 |
82 |
94 case "$OUTFORMAT" in |
83 case "$OUTFORMAT" in |
95 dvi) |
84 dvi) |
96 check_root && \ |
85 check_root && \ |
97 run_latex |
86 run_latex |
130 check_root && \ |
119 check_root && \ |
131 run_thumbpdf |
120 run_thumbpdf |
132 RC="$?" |
121 RC="$?" |
133 ;; |
122 ;; |
134 sty) |
123 sty) |
135 update_styles |
124 copy_styles |
136 RC="$?" |
125 RC="$?" |
137 ;; |
126 ;; |
138 *) |
127 *) |
139 fail "Bad output format '$OUTFORMAT'" |
128 fail "Bad output format '$OUTFORMAT'" |
140 ;; |
129 ;; |