1.1 --- a/lib/Tools/convert Tue Apr 08 15:47:05 2008 +0200
1.2 +++ b/lib/Tools/convert Tue Apr 08 15:47:10 2008 +0200
1.3 @@ -35,8 +35,5 @@
1.4
1.5 ## main
1.6
1.7 -#set by configure
1.8 -AUTO_PERL=perl
1.9 -
1.10 find $SPECS \( -name \*.ML \) -print | \
1.11 - xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl"
1.12 + xargs perl -w "$ISABELLE_HOME/lib/scripts/convert.pl"
2.1 --- a/lib/Tools/dimacs2hol Tue Apr 08 15:47:05 2008 +0200
2.2 +++ b/lib/Tools/dimacs2hol Tue Apr 08 15:47:10 2008 +0200
2.3 @@ -45,7 +45,4 @@
2.4
2.5 ## main
2.6
2.7 -#set by configure
2.8 -AUTO_PERL=perl
2.9 -
2.10 -"$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@"
2.11 +exec perl -w "$ISABELLE_HOME/lib/scripts/dimacs2hol.pl" "$@"
3.1 --- a/lib/Tools/fixheaders Tue Apr 08 15:47:05 2008 +0200
3.2 +++ b/lib/Tools/fixheaders Tue Apr 08 15:47:10 2008 +0200
3.3 @@ -33,8 +33,5 @@
3.4
3.5 ## main
3.6
3.7 -#set by configure
3.8 -AUTO_PERL=perl
3.9 -
3.10 find $SPECS -name \*.thy -print | \
3.11 - xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl"
3.12 + xargs perl -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl"
4.1 --- a/lib/Tools/keywords Tue Apr 08 15:47:05 2008 +0200
4.2 +++ b/lib/Tools/keywords Tue Apr 08 15:47:10 2008 +0200
4.3 @@ -57,9 +57,6 @@
4.4
4.5 ## main
4.6
4.7 -#set by configure
4.8 -AUTO_PERL=perl
4.9 -
4.10 SESSIONS=""
4.11 for LOG in $LOGS
4.12 do
4.13 @@ -80,4 +77,4 @@
4.14 fi
4.15 echo
4.16 done | \
4.17 -"$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"
4.18 +perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"
5.1 --- a/lib/Tools/latex Tue Apr 08 15:47:05 2008 +0200
5.2 +++ b/lib/Tools/latex Tue Apr 08 15:47:10 2008 +0200
5.3 @@ -72,9 +72,6 @@
5.4
5.5 # operations
5.6
5.7 -#set by configure
5.8 -AUTO_PERL=perl
5.9 -
5.10 function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
5.11 function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
5.12 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
5.13 @@ -86,16 +83,16 @@
5.14 for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
5.15 do
5.16 TARGET="$DIR"/$(basename "$STYLEFILE")
5.17 - "$AUTO_PERL" -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
5.18 + perl -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
5.19 done
5.20 }
5.21
5.22 function extract_syms ()
5.23 {
5.24 - "$AUTO_PERL" -n \
5.25 + perl -n \
5.26 -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \
5.27 "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > "$DIR/syms.lst"
5.28 - "$AUTO_PERL" -n \
5.29 + perl -n \
5.30 -e 'm,\\newcommand\{\\isactrl(\w+)\}, && print "$1\n";' \
5.31 "$ISABELLE_HOME/lib/texinputs/isabelle.sty" > "$DIR/ctrls.lst"
5.32 }
6.1 --- a/lib/Tools/logo Tue Apr 08 15:47:05 2008 +0200
6.2 +++ b/lib/Tools/logo Tue Apr 08 15:47:10 2008 +0200
6.3 @@ -70,12 +70,9 @@
6.4 OUTFILE="isabelle${OUTFILE}.eps"
6.5 fi
6.6
6.7 -#set by configure
6.8 -AUTO_PERL=perl
6.9 -
6.10 if [ "$OUTFILE" = "-" ]; then
6.11 - "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
6.12 + perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
6.13 else
6.14 [ -z "$QUIET" ] && echo "$OUTFILE" >&2
6.15 - "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
6.16 + perl -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
6.17 fi
7.1 --- a/lib/Tools/unsymbolize Tue Apr 08 15:47:05 2008 +0200
7.2 +++ b/lib/Tools/unsymbolize Tue Apr 08 15:47:10 2008 +0200
7.3 @@ -34,8 +34,5 @@
7.4
7.5 ## main
7.6
7.7 -#set by configure
7.8 -AUTO_PERL=perl
7.9 -
7.10 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
7.11 - xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
7.12 + xargs perl -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
8.1 --- a/lib/scripts/feeder Tue Apr 08 15:47:05 2008 +0200
8.2 +++ b/lib/scripts/feeder Tue Apr 08 15:47:10 2008 +0200
8.3 @@ -75,7 +75,4 @@
8.4
8.5 ## main
8.6
8.7 -#set by configure
8.8 -AUTO_PERL=perl
8.9 -
8.10 -exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"
8.11 +exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"
9.1 --- a/lib/scripts/timestart.bash Tue Apr 08 15:47:05 2008 +0200
9.2 +++ b/lib/scripts/timestart.bash Tue Apr 08 15:47:10 2008 +0200
9.3 @@ -7,13 +7,10 @@
9.4
9.5 TIMES_RESULT=""
9.6
9.7 -#set by configure
9.8 -AUTO_PERL=perl
9.9 -
9.10 function get_times () {
9.11 local TMP="/tmp/get_times$$"
9.12 times > "$TMP" # No pipe here!
9.13 - TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | "$AUTO_PERL" -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
9.14 + TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | perl -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
9.15 rm -f "$TMP"
9.16 }
9.17