removed obsolete AUTO_PERL feature;
authorwenzelm
Tue Apr 08 15:47:10 2008 +0200 (2008-04-08)
changeset 26576fc76b7b79ba9
parent 26575 042617a1c86c
child 26577 50f47cc2af72
removed obsolete AUTO_PERL feature;
lib/Tools/convert
lib/Tools/dimacs2hol
lib/Tools/fixheaders
lib/Tools/keywords
lib/Tools/latex
lib/Tools/logo
lib/Tools/unsymbolize
lib/scripts/feeder
lib/scripts/timestart.bash
     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