diff options
Diffstat (limited to 'math/isabelle/files')
49 files changed, 37 insertions, 1301 deletions
diff --git a/math/isabelle/files/patch-bin-Isabelle b/math/isabelle/files/patch-bin-Isabelle deleted file mode 100644 index 86b306d14cee..000000000000 --- a/math/isabelle/files/patch-bin-Isabelle +++ /dev/null @@ -1,8 +0,0 @@ ---- ./bin/Isabelle.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/Isabelle Sun Sep 2 16:05:40 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: Isabelle,v 1.30 2005/05/17 07:58:47 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen diff --git a/math/isabelle/files/patch-bin-isabelle b/math/isabelle/files/patch-bin-isabelle deleted file mode 100644 index 62b441a378bb..000000000000 --- a/math/isabelle/files/patch-bin-isabelle +++ /dev/null @@ -1,8 +0,0 @@ ---- ./bin/isabelle.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/isabelle Sun Sep 2 16:05:44 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isabelle,v 1.46 2005/05/17 07:58:47 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen diff --git a/math/isabelle/files/patch-bin-isabelle_interface b/math/isabelle/files/patch-bin-isabelle_interface deleted file mode 100644 index a8ec33a1f2a3..000000000000 --- a/math/isabelle/files/patch-bin-isabelle_interface +++ /dev/null @@ -1,23 +0,0 @@ ---- ./bin/isabelle-interface.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/isabelle-interface Sun Sep 2 16:05:48 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isabelle-interface,v 1.8 2005/05/17 16:10:33 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -16,12 +16,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-bin-isabelle_process b/math/isabelle/files/patch-bin-isabelle_process deleted file mode 100644 index 92c308f02e7e..000000000000 --- a/math/isabelle/files/patch-bin-isabelle_process +++ /dev/null @@ -1,32 +0,0 @@ ---- bin/isabelle-process.orig Sat Jan 12 16:42:22 2008 -+++ bin/isabelle-process Sat Jan 12 16:42:58 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isabelle-process,v 1.17 2006/12/04 20:33:36 aspinall Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -16,12 +16,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" -@@ -49,7 +49,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-bin-isatool b/math/isabelle/files/patch-bin-isatool deleted file mode 100644 index a536b5cf75ff..000000000000 --- a/math/isabelle/files/patch-bin-isatool +++ /dev/null @@ -1,32 +0,0 @@ ---- ./bin/isatool.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/isatool Sun Sep 2 16:05:57 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isatool,v 1.22 2005/05/17 07:58:47 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -16,12 +16,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG TOOL [ARGS ...]" -@@ -49,7 +49,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-build b/math/isabelle/files/patch-build deleted file mode 100644 index 0d1a9733276c..000000000000 --- a/math/isabelle/files/patch-build +++ /dev/null @@ -1,32 +0,0 @@ ---- build.orig Sat Jan 12 16:44:25 2008 -+++ build Sat Jan 12 16:46:08 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: build,v 1.36 2005/12/01 17:41:46 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -23,12 +23,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [LOGICS ...]" -@@ -46,7 +46,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-etc-settings b/math/isabelle/files/patch-etc-settings index 56be18daf783..34ecb3965692 100644 --- a/math/isabelle/files/patch-etc-settings +++ b/math/isabelle/files/patch-etc-settings @@ -1,6 +1,6 @@ ---- etc/settings.orig Sat Jan 12 16:47:09 2008 -+++ etc/settings Sat Jan 12 16:56:24 2008 -@@ -16,60 +16,27 @@ +--- etc/settings.orig 2008-07-28 15:10:38.000000000 +1000 ++++ etc/settings 2008-07-28 15:22:08.000000000 +1000 +@@ -16,70 +16,36 @@ # not invent new ML system names unless you know what you are doing. # Only one of the sections below should be activated. @@ -15,7 +15,7 @@ - "/opt/polyml/$ML_PLATFORM" \ - $POLY_HOME) -ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") --ML_OPTIONS="-H 500" +-ML_OPTIONS="-H 200" -ML_DBASE="" - -# Poly/ML 5.1 @@ -69,7 +69,18 @@ #ML_OPTIONS="-noinit" #ML_SUFFIX=".psv" #ML_PLATFORM="" -@@ -155,7 +122,7 @@ + +- + ### + ### Interactive sessions (cf. isatool tty) + ### + +-ISABELLE_LINE_EDITOR="" ++ISABELLE_LINE_EDITOR="%%LINE_EDIT%%" + [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" + [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" + +@@ -154,7 +120,7 @@ ### # Where to look for docs (multiple dirs separated by ':'). @@ -78,15 +89,29 @@ # Preferred document format ISABELLE_DOC_FORMAT=pdf -@@ -190,6 +157,7 @@ +@@ -189,6 +155,8 @@ # Proof General path, look in a variety of places ISABELLE_INTERFACE=$(choosefrom \ ++ "%%PREFIX%%/lib/xemacs/site-lisp/ProofGeneral/isar/interface" \ + "%%PREFIX%%/bin/proofgeneral" \ "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ "$ISABELLE_HOME/../ProofGeneral/isar/interface" \ "/usr/local/ProofGeneral/isar/interface" \ -@@ -223,26 +191,26 @@ +@@ -211,9 +179,9 @@ + ## Set HOME only for tools you have installed! + + # External provers +-E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "") +-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "") +-SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "") ++E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "%%PREFIX%%/E" "") ++VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "%%PREFIX%%/Vampire" "") ++SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "%%PREFIX%%/SPASS" "") + + # HOL4 proof objects (cf. Isabelle/src/HOL/Import) + #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs" +@@ -224,26 +192,26 @@ #SVC_MACHINE=sparc-sun-solaris # Mucke (mu-calculus model checker) @@ -119,13 +144,3 @@ # For configuring HOL/Matrix/cplex # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver. -@@ -254,6 +222,6 @@ - #GLPK_PATH=glpsol - - # External provers --E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "") --VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "") --SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "") -+E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "%%PREFIX%%/E" "") -+VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "%%PREFIX%%/Vampire" "") -+SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "%%PREFIX%%/SPASS" "") diff --git a/math/isabelle/files/patch-lib-Tools-browser b/math/isabelle/files/patch-lib-Tools-browser deleted file mode 100644 index a0941efa88e6..000000000000 --- a/math/isabelle/files/patch-lib-Tools-browser +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/browser.orig Sat Jan 12 16:56:56 2008 -+++ lib/Tools/browser Sat Jan 12 16:58:42 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: browser,v 1.17 2006/09/18 17:12:41 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [GRAPHFILE]" -@@ -20,7 +20,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-codegen b/math/isabelle/files/patch-lib-Tools-codegen deleted file mode 100644 index 786015002556..000000000000 --- a/math/isabelle/files/patch-lib-Tools-codegen +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/codegen.orig Sat Jan 12 17:19:17 2008 -+++ lib/Tools/codegen Sat Jan 12 17:19:37 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: codegen,v 1.5 2007/11/21 13:18:23 haftmann Exp $ - # Author: Florian Haftmann, TUM -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG IMAGE THY SERI" diff --git a/math/isabelle/files/patch-lib-Tools-convert b/math/isabelle/files/patch-lib-Tools-convert deleted file mode 100644 index 97a0515e6ee2..000000000000 --- a/math/isabelle/files/patch-lib-Tools-convert +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/convert.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/convert Sun Sep 2 15:48:00 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: convert,v 1.5 2005/04/26 17:50:57 wenzelm Exp $ - # Author: David von Oheimb, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-dimacs2hol b/math/isabelle/files/patch-lib-Tools-dimacs2hol deleted file mode 100644 index 2cff3a23e8a1..000000000000 --- a/math/isabelle/files/patch-lib-Tools-dimacs2hol +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/dimacs2hol.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/dimacs2hol Sun Sep 2 15:48:05 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: dimacs2hol,v 1.3 2005/04/26 17:50:57 wenzelm Exp $ - # Author: Tjark Weber -@@ -11,7 +11,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG FILES" diff --git a/math/isabelle/files/patch-lib-Tools-display b/math/isabelle/files/patch-lib-Tools-display deleted file mode 100644 index beebd48dc0f7..000000000000 --- a/math/isabelle/files/patch-lib-Tools-display +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/display.orig Sat Jan 12 16:57:02 2008 -+++ lib/Tools/display Sat Jan 12 17:00:11 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: display,v 1.10 2006/11/13 17:19:24 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] FILE" -@@ -21,7 +21,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-doc b/math/isabelle/files/patch-lib-Tools-doc deleted file mode 100644 index 47790edec2c6..000000000000 --- a/math/isabelle/files/patch-lib-Tools-doc +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/Tools/doc.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/doc Sun Sep 2 15:48:14 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: doc,v 1.13 2005/04/13 16:48:06 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [DOC]" -@@ -18,7 +18,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-document b/math/isabelle/files/patch-lib-Tools-document deleted file mode 100644 index f2553f4c41ee..000000000000 --- a/math/isabelle/files/patch-lib-Tools-document +++ /dev/null @@ -1,44 +0,0 @@ ---- ./lib/Tools/document.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/document Sun Sep 2 15:48:20 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: document,v 1.22 2005/08/16 11:42:15 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [DIR]" -@@ -25,7 +25,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 -@@ -88,7 +88,7 @@ - - # tagged region markup - --function prep_tags () -+prep_tags () - { - ( - IFS="," -@@ -115,7 +115,7 @@ - - # prepare document - --function pre_latex () -+pre_latex () - { - local FMT="$1" - [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log diff --git a/math/isabelle/files/patch-lib-Tools-expandshort b/math/isabelle/files/patch-lib-Tools-expandshort deleted file mode 100644 index d8f622317fa2..000000000000 --- a/math/isabelle/files/patch-lib-Tools-expandshort +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/expandshort.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/expandshort Sun Sep 2 15:48:24 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: expandshort,v 1.15 2005/04/26 17:50:57 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-findlogics b/math/isabelle/files/patch-lib-Tools-findlogics deleted file mode 100644 index e992cb876e60..000000000000 --- a/math/isabelle/files/patch-lib-Tools-findlogics +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/findlogics.orig Sat Jan 12 16:57:07 2008 -+++ lib/Tools/findlogics Sat Jan 12 17:00:42 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: findlogics,v 1.9 2005/10/08 18:15:31 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG=$(basename "$0") - --function usage() -+usage() - { - echo - echo "Usage: $PRG" diff --git a/math/isabelle/files/patch-lib-Tools-fixcpure b/math/isabelle/files/patch-lib-Tools-fixcpure deleted file mode 100644 index 987dee280477..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixcpure +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixcpure.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixcpure Sun Sep 2 15:48:31 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixcpure,v 1.2 2005/04/26 17:50:57 wenzelm Exp $ - # Author: Makarius -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-fixgreek b/math/isabelle/files/patch-lib-Tools-fixgreek deleted file mode 100644 index d182ad0a897e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixgreek +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixgreek.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixgreek Sun Sep 2 15:48:35 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixgreek,v 1.4 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Sebastian Skalberg, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-fixheaders b/math/isabelle/files/patch-lib-Tools-fixheaders deleted file mode 100644 index a73ea7a9bb17..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixheaders +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixheaders.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixheaders Sun Sep 2 15:48:38 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixheaders,v 1.2 2005/07/06 08:34:07 wenzelm Exp $ - # Author: Florian Haftmann, TUM -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-fixsome b/math/isabelle/files/patch-lib-Tools-fixsome deleted file mode 100644 index 6af6a93a2f3e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixsome +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixsome.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixsome Sun Sep 2 15:48:42 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixsome,v 1.7 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-getenv b/math/isabelle/files/patch-lib-Tools-getenv deleted file mode 100644 index 310071e543ed..000000000000 --- a/math/isabelle/files/patch-lib-Tools-getenv +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/getenv.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/getenv Sun Sep 2 15:48:46 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: getenv,v 1.11 2005/09/01 20:49:18 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [VARNAMES ...]" diff --git a/math/isabelle/files/patch-lib-Tools-install b/math/isabelle/files/patch-lib-Tools-install deleted file mode 100644 index 8c61bcea857e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-install +++ /dev/null @@ -1,54 +0,0 @@ ---- ./lib/Tools/install.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/install Sun Sep 2 15:52:30 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: install,v 1.25 2005/07/01 12:41:57 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG=$(basename "$0") - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS]" -@@ -24,7 +24,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 -@@ -71,18 +71,6 @@ - - # standalone binaries - --#set by configure --AUTO_BASH=bash -- --case "$AUTO_BASH" in -- /*) -- BASH="$AUTO_BASH" -- ;; -- *) -- BASH="/usr/bin/env bash" -- ;; --esac -- - if [ -n "$BINDIR" ]; then - mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" - -@@ -92,7 +80,7 @@ - DIST="$DISTDIR/bin/$NAME" - echo "installing $BIN" - rm -f "$BIN" -- echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN" -+ echo "#!/bin/sh" > "$BIN" || fail "Cannot write file: $BIN" - echo >> "$BIN" - echo "exec \"$DIST\" \"\$@\"" >> "$BIN" - chmod +x "$BIN" diff --git a/math/isabelle/files/patch-lib-Tools-keywords b/math/isabelle/files/patch-lib-Tools-keywords deleted file mode 100644 index 95494253e834..000000000000 --- a/math/isabelle/files/patch-lib-Tools-keywords +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/keywords.orig Sat Jan 12 17:16:34 2008 -+++ lib/Tools/keywords Sat Jan 12 17:17:21 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: keywords,v 1.3 2007/10/07 11:32:15 wenzelm Exp $ - # Author: Makarius -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [LOGS ...]" diff --git a/math/isabelle/files/patch-lib-Tools-latex b/math/isabelle/files/patch-lib-Tools-latex deleted file mode 100644 index 8c4881b113f8..000000000000 --- a/math/isabelle/files/patch-lib-Tools-latex +++ /dev/null @@ -1,65 +0,0 @@ ---- ./lib/Tools/latex.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/latex Sun Sep 2 15:48:54 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: latex,v 1.27 2005/07/19 15:21:45 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [FILE]" -@@ -23,7 +23,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 -@@ -67,7 +67,7 @@ - FILEBASE=$(basename "$FILE" .tex) - [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" - --function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } -+check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } - - - # operations -@@ -75,13 +75,13 @@ - #set by configure - AUTO_PERL=perl - --function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } --function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } --function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } --function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } --function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } --function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } --function copy_styles () -+run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } -+run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } -+run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } -+run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } -+run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } -+run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } -+copy_styles () - { - for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty - do -@@ -90,7 +90,7 @@ - done - } - --function extract_syms () -+extract_syms () - { - "$AUTO_PERL" -n \ - -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ diff --git a/math/isabelle/files/patch-lib-Tools-logo b/math/isabelle/files/patch-lib-Tools-logo deleted file mode 100644 index 96d4abb02507..000000000000 --- a/math/isabelle/files/patch-lib-Tools-logo +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/Tools/logo.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/logo Sun Sep 2 15:49:00 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: logo,v 1.10 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] NAME" -@@ -22,7 +22,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-make b/math/isabelle/files/patch-lib-Tools-make deleted file mode 100644 index 38124254928e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-make +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/make.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/make Sun Sep 2 15:49:08 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: make,v 1.9 2004/06/21 08:25:57 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [ARGS ...]" diff --git a/math/isabelle/files/patch-lib-Tools-makeall b/math/isabelle/files/patch-lib-Tools-makeall deleted file mode 100644 index 01a5e28d69eb..000000000000 --- a/math/isabelle/files/patch-lib-Tools-makeall +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/makeall.orig Sat Jan 12 16:57:16 2008 -+++ lib/Tools/makeall Sat Jan 12 17:01:23 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: makeall,v 1.20 2005/12/01 17:41:46 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -14,7 +14,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [ARGS ...]" -@@ -24,7 +24,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-mkdir b/math/isabelle/files/patch-lib-Tools-mkdir deleted file mode 100644 index f4c113000e98..000000000000 --- a/math/isabelle/files/patch-lib-Tools-mkdir +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/mkdir.orig Sat Jan 12 16:57:23 2008 -+++ lib/Tools/mkdir Sat Jan 12 17:02:14 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: mkdir,v 1.45 2007/11/12 10:18:51 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [LOGIC] NAME" -@@ -27,7 +27,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-mkproject b/math/isabelle/files/patch-lib-Tools-mkproject deleted file mode 100644 index 069af7d50cb9..000000000000 --- a/math/isabelle/files/patch-lib-Tools-mkproject +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/mkproject.orig Sat Jan 12 17:18:15 2008 -+++ lib/Tools/mkproject Sat Jan 12 17:18:41 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: mkproject,v 1.2 2007/08/09 17:19:23 wenzelm Exp $ - # Author: David Aspinall and Makarius Wenzel -@@ -7,7 +7,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG NAME" diff --git a/math/isabelle/files/patch-lib-Tools-print b/math/isabelle/files/patch-lib-Tools-print deleted file mode 100644 index b64170ce1ee6..000000000000 --- a/math/isabelle/files/patch-lib-Tools-print +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/Tools/print.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/print Sun Sep 2 15:49:21 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: print,v 1.2 2004/06/29 09:21:18 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] FILE" -@@ -21,7 +21,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-unsymbolize b/math/isabelle/files/patch-lib-Tools-unsymbolize deleted file mode 100644 index 35a0665b887a..000000000000 --- a/math/isabelle/files/patch-lib-Tools-unsymbolize +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/unsymbolize.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/unsymbolize Sun Sep 2 15:49:24 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: unsymbolize,v 1.6 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-usedir b/math/isabelle/files/patch-lib-Tools-usedir deleted file mode 100644 index 219da65abdcf..000000000000 --- a/math/isabelle/files/patch-lib-Tools-usedir +++ /dev/null @@ -1,48 +0,0 @@ ---- lib/Tools/usedir.orig Sat Jan 12 16:57:29 2008 -+++ lib/Tools/usedir Sat Jan 12 17:03:34 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: usedir,v 1.67 2007/10/30 09:52:26 haftmann Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] LOGIC NAME" -@@ -43,18 +43,18 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 - } - --function check_bool() -+check_bool() - { - [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\"" - } - --function check_number() -+check_number() - { - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" - } -@@ -82,7 +82,7 @@ - PROOFS=0 - VERBOSE=false - --function getoptions() -+getoptions() - { - OPTIND=1 - while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT diff --git a/math/isabelle/files/patch-lib-Tools-version b/math/isabelle/files/patch-lib-Tools-version deleted file mode 100644 index 0e7a6c9fc596..000000000000 --- a/math/isabelle/files/patch-lib-Tools-version +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/Tools/version.orig Sat Jan 12 16:57:34 2008 -+++ lib/Tools/version Sat Jan 12 17:03:48 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: version,v 1.2 2004/06/21 08:25:57 kleing Exp $ - # Author: Stefan Berghofer, TU Muenchen diff --git a/math/isabelle/files/patch-lib-scripts-configure b/math/isabelle/files/patch-lib-scripts-configure deleted file mode 100644 index 60bab756414c..000000000000 --- a/math/isabelle/files/patch-lib-scripts-configure +++ /dev/null @@ -1,15 +0,0 @@ ---- lib/scripts/configure.orig Fri Sep 14 18:00:10 2007 -+++ lib/scripts/configure Fri Sep 14 18:00:21 2007 -@@ -8,11 +8,5 @@ - ## patch scripts - - cd "`dirname "$0"`" -+exec sh lib/scripts/patch-scripts.bash - --if bash -c : --then -- bash lib/scripts/patch-scripts.bash --else -- echo "FATAL ERROR: bash not found!" -- exit 2 --fi diff --git a/math/isabelle/files/patch-lib-scripts-feeder b/math/isabelle/files/patch-lib-scripts-feeder deleted file mode 100644 index 2c0963651e3a..000000000000 --- a/math/isabelle/files/patch-lib-scripts-feeder +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/scripts/feeder.orig Sun Sep 2 15:12:50 2007 -+++ ./lib/scripts/feeder Sun Sep 2 15:54:12 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: feeder,v 1.10 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -11,7 +11,7 @@ - PRG="$(basename "$0")" - DIR="$(dirname "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS]" -@@ -27,7 +27,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-scripts-fileindent b/math/isabelle/files/patch-lib-scripts-fileindent deleted file mode 100644 index 39a7d8624656..000000000000 --- a/math/isabelle/files/patch-lib-scripts-fileindent +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/scripts/fileident.orig Sat Jan 12 17:20:26 2008 -+++ lib/scripts/fileident Sat Jan 12 17:20:38 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fileident,v 1.1 2007/07/17 20:51:27 wenzelm Exp $ - # diff --git a/math/isabelle/files/patch-lib-scripts-getsettings b/math/isabelle/files/patch-lib-scripts-getsettings deleted file mode 100644 index 49fea452c414..000000000000 --- a/math/isabelle/files/patch-lib-scripts-getsettings +++ /dev/null @@ -1,30 +0,0 @@ ---- lib/scripts/getsettings.orig Sat Jan 12 17:08:58 2008 -+++ lib/scripts/getsettings Sat Jan 12 17:10:17 2008 -@@ -27,10 +27,9 @@ - - #users tend to put strange things in here ... - unset ENV --unset BASH_ENV - - #support easy settings --function choosefrom () -+choosefrom () - { - local RESULT="" - local FILE="" -@@ -45,13 +44,13 @@ - } - - #get actual settings --source "$ISABELLE_HOME/etc/settings" || exit 2 -+. "$ISABELLE_HOME/etc/settings" || exit 2 - ISABELLE_SITE_SETTINGS_PRESENT=true - - [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ - { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; } - [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \ -- { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; } -+ { . "$ISABELLE_HOME_USER/etc/settings" || exit 2; } - - #ML system identifier - if [ -z "$ML_PLATFORM" ]; then diff --git a/math/isabelle/files/patch-lib-scripts-patch_scripts.bash b/math/isabelle/files/patch-lib-scripts-patch_scripts.bash deleted file mode 100644 index 712f12891bac..000000000000 --- a/math/isabelle/files/patch-lib-scripts-patch_scripts.bash +++ /dev/null @@ -1,37 +0,0 @@ ---- lib/scripts/patch-scripts.bash.orig Sun Sep 2 15:55:18 2007 -+++ lib/scripts/patch-scripts.bash Sun Sep 2 16:06:41 2007 -@@ -3,12 +3,12 @@ - # Author: Markus Wenzel, TU Muenchen - # - # patch-scripts.bash - relocate interpreter paths of executable scripts and --# insert AUTO_BASH/AUTO_PERL values -+# insert AUTO_PERL values - # - - ## find binaries - --function findbin() -+findbin() - { - local BASE="$1" - local BINARY="" -@@ -29,17 +29,14 @@ - - ## main - --[ -z "$BASH_PATH" ] && BASH_PATH=$(findbin bash) - [ -z "$PERL_PATH" ] && PERL_PATH=$(findbin perl) --[ -z "$AUTO_BASH" ] && AUTO_BASH="$BASH_PATH" - [ -z "$AUTO_PERL" ] && AUTO_PERL="$PERL_PATH" - - for FILE in $(find . -type f -print) - do - if [ -x "$FILE" ]; then -- sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \ -- -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \ -- -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~" -+ sed -e "s:^#!.*/perl:#!$PERL_PATH:" \ -+ -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~" - if cmp -s "$FILE" "$FILE~~"; then - rm "$FILE~~" - else diff --git a/math/isabelle/files/patch-lib-scripts-polyml_platform b/math/isabelle/files/patch-lib-scripts-polyml_platform deleted file mode 100644 index 911d496b6a1f..000000000000 --- a/math/isabelle/files/patch-lib-scripts-polyml_platform +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/scripts/polyml-platform.orig Sat Jan 12 17:09:07 2008 -+++ lib/scripts/polyml-platform Sat Jan 12 17:11:51 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: polyml-platform,v 1.6 2007/11/08 19:07:58 wenzelm Exp $ - # diff --git a/math/isabelle/files/patch-lib-scripts-polyml_version b/math/isabelle/files/patch-lib-scripts-polyml_version deleted file mode 100644 index cd6be76c2ecd..000000000000 --- a/math/isabelle/files/patch-lib-scripts-polyml_version +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/scripts/polyml-version.orig Sat Jan 12 17:09:13 2008 -+++ lib/scripts/polyml-version Sat Jan 12 17:15:41 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: polyml-version,v 1.5 2006/12/05 17:32:54 wenzelm Exp $ - # diff --git a/math/isabelle/files/patch-lib-scripts-run_mosml b/math/isabelle/files/patch-lib-scripts-run_mosml deleted file mode 100644 index bc7fa92d97af..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_mosml +++ /dev/null @@ -1,35 +0,0 @@ ---- lib/scripts/run-mosml.orig Mon Jun 21 18:25:58 2004 -+++ lib/scripts/run-mosml Sun Sep 2 17:14:13 2007 -@@ -1,16 +1,14 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-mosml,v 1.8 2004/06/21 08:25:58 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen - # - # Moscow ML 2.00 startup script - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 -@@ -37,6 +35,13 @@ - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } - fi - -+SAVE_OUTFILE="$OUTFILE" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+OUTFILE="$SAVE_OUTFILE" -+MLTEXT="$SAVE_MLTEXT" -+NOWRITE="$SAVE_NOWRITE" - - ## run it! - diff --git a/math/isabelle/files/patch-lib-scripts-run_polyml b/math/isabelle/files/patch-lib-scripts-run_polyml deleted file mode 100644 index f2ae5e4a57a2..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_polyml +++ /dev/null @@ -1,45 +0,0 @@ ---- lib/scripts/run-polyml.orig Sun Oct 21 04:31:50 2007 -+++ lib/scripts/run-polyml Sat Jan 12 18:01:17 2008 -@@ -5,18 +5,15 @@ - # - # Poly/ML startup script. - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- -- - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_file() -+check_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,6 +22,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## Poly/ML executable and database - diff --git a/math/isabelle/files/patch-lib-scripts-run_polyml_5.0 b/math/isabelle/files/patch-lib-scripts-run_polyml_5.0 deleted file mode 100644 index 4ece1175bd54..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_polyml_5.0 +++ /dev/null @@ -1,50 +0,0 @@ ---- lib/scripts/run-polyml-5.0.orig Sun Oct 21 04:32:23 2007 -+++ lib/scripts/run-polyml-5.0 Sat Jan 12 18:01:28 2008 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-polyml-5.0,v 1.9 2007/10/20 18:32:23 wenzelm Exp $ - # Author: Makarius - # - # Poly/ML startup script (for 5.0) - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_file() -+check_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,6 +23,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## compiler executables and libraries - diff --git a/math/isabelle/files/patch-lib-scripts-run_polyml_5.1 b/math/isabelle/files/patch-lib-scripts-run_polyml_5.1 deleted file mode 100644 index 212bf2b467fa..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_polyml_5.1 +++ /dev/null @@ -1,50 +0,0 @@ ---- lib/scripts/run-polyml-5.1.orig Tue Nov 20 21:42:15 2007 -+++ lib/scripts/run-polyml-5.1 Sat Jan 12 18:01:39 2008 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-polyml-5.1,v 1.7 2007/11/20 10:42:15 wenzelm Exp $ - # Author: Makarius - # - # Poly/ML startup script (for 5.1) - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_file() -+check_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,6 +23,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## compiler executables and libraries - diff --git a/math/isabelle/files/patch-lib-scripts-run_poplogml b/math/isabelle/files/patch-lib-scripts-run_poplogml deleted file mode 100644 index f0a27abc35f9..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_poplogml +++ /dev/null @@ -1,59 +0,0 @@ ---- lib/scripts/run-poplogml.orig Tue Oct 11 21:28:04 2005 -+++ lib/scripts/run-poplogml Sat Jan 12 18:01:54 2008 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-poplogml,v 1.5 2005/10/11 11:28:04 wenzelm Exp $ - # Author: Makarius - # - # Poplog/PML startup script (version 15.6/2.1). - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_mlhome_file() -+check_mlhome_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,7 +23,7 @@ - fi - } - --function check_heap_file() -+check_heap_file() - { - if [ ! -f "$1" ]; then - echo "Expected to find ML heap file $1" >&2 -@@ -35,6 +33,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## prepare databases - diff --git a/math/isabelle/files/patch-lib-scripts-run_smlnj b/math/isabelle/files/patch-lib-scripts-run_smlnj index 5d3b82fedbbf..687fb62bacaa 100644 --- a/math/isabelle/files/patch-lib-scripts-run_smlnj +++ b/math/isabelle/files/patch-lib-scripts-run_smlnj @@ -1,43 +1,10 @@ ---- lib/scripts/run-smlnj.orig Mon Jun 21 18:25:58 2004 -+++ lib/scripts/run-smlnj Fri Sep 14 18:01:25 2007 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-smlnj,v 1.28 2004/06/21 08:25:58 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen - # - # SML/NJ startup script (for 110 or later). +--- lib/scripts/run-smlnj.orig 2004-06-21 18:25:58.000000000 +1000 ++++ lib/scripts/run-smlnj 2008-07-29 15:49:30.000000000 +1000 +@@ -39,11 +39,10 @@ --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_mlhome_file() -+check_mlhome_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,7 +23,7 @@ - fi - } - --function check_heap_file() -+check_heap_file() - { - if [ ! -f "$1" ]; then - echo "Expected to find ML heap file $1" >&2 -@@ -40,10 +38,8 @@ ## compiler binaries ++export SMLNJ_DEVEL=yes SML="$ML_HOME/sml" -ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys" @@ -46,22 +13,7 @@ -@@ -76,6 +72,14 @@ - FEEDER_OPTS="-q" - fi - -+SAVE_OUTFILE="$OUTFILE" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+OUTFILE="$SAVE_OUTFILE" -+MLTEXT="$SAVE_MLTEXT" -+NOWRITE="$SAVE_NOWRITE" -+ - "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ - { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } - RC="$?" -@@ -84,8 +88,7 @@ +@@ -84,8 +83,7 @@ ## fix heap file name and permissions if [ -n "$OUTFILE" ]; then diff --git a/math/isabelle/files/patch-lib-scripts-timestart.bash b/math/isabelle/files/patch-lib-scripts-timestart.bash deleted file mode 100644 index bba13d73fc06..000000000000 --- a/math/isabelle/files/patch-lib-scripts-timestart.bash +++ /dev/null @@ -1,16 +0,0 @@ ---- lib/scripts/timestart.bash.orig Thu Dec 8 01:23:22 2005 -+++ lib/scripts/timestart.bash Sat Jan 12 17:53:32 2008 -@@ -10,9 +10,11 @@ - #set by configure - AUTO_PERL=perl - --function get_times () { -- local TMP="/tmp/get_times$$" -+get_times () { -+ local TMP SECONDS -+ TMP="/tmp/get_times$$" - times > "$TMP" # No pipe here! -+ SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` )) - 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')" - rm -f "$TMP" - } diff --git a/math/isabelle/files/patch-lib-scripts-timestop.bash b/math/isabelle/files/patch-lib-scripts-timestop.bash deleted file mode 100644 index fc672fb7d325..000000000000 --- a/math/isabelle/files/patch-lib-scripts-timestop.bash +++ /dev/null @@ -1,44 +0,0 @@ ---- lib/scripts/timestop.bash.orig Fri Dec 2 04:44:47 2005 -+++ lib/scripts/timestop.bash Sat Jan 12 17:54:13 2008 -@@ -7,28 +7,29 @@ - - TIMES_REPORT="" - --function show_times () -+show_times () - { -- local TIMES_START="$TIMES_RESULT" -+ local TIMES_START TIMES_STOP KIND START STOP TIME SECS MINUTES HOURS \ -+ KIND_NAME RESULT -+ -+ TIMES_START="$TIMES_RESULT" - get_times -- local TIMES_STOP="$TIMES_RESULT" -- local KIND -+ TIMES_STOP="$TIMES_RESULT" - for KIND in 1 2 - do -- local START=$(echo "$TIMES_START" | cut -d " " -f $KIND) -- local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) -+ START=$(echo "$TIMES_START" | cut -d " " -f $KIND) -+ STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) - -- local TIME=$[ $STOP - $START ] -- local SECS=$[ $TIME % 60 ] -+ TIME=$(( $STOP - $START )) -+ SECS=$(( $TIME % 60 )) - [ $SECS -lt 10 ] && SECS="0$SECS" -- local MINUTES=$[ ($TIME / 60) % 60 ] -+ MINUTES=$(( ($TIME / 60) % 60 )) - [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" -- local HOURS=$[ $TIME / 3600 ] -+ HOURS=$(( $TIME / 3600 )) - -- local KIND_NAME - [ "$KIND" = 1 ] && KIND_NAME="elapsed time" - [ "$KIND" = 2 ] && KIND_NAME="cpu time" -- local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" -+ RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" - - if [ -z "$TIMES_REPORT" ]; then - TIMES_REPORT="$RESULT" diff --git a/math/isabelle/files/patch-src-Pure-mk b/math/isabelle/files/patch-src-Pure-mk deleted file mode 100644 index e23ecd5d35ef..000000000000 --- a/math/isabelle/files/patch-src-Pure-mk +++ /dev/null @@ -1,26 +0,0 @@ ---- src/Pure/mk.orig Sat Jan 12 17:35:00 2008 -+++ src/Pure/mk Sat Jan 12 17:36:05 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: mk,v 1.32 2007/01/04 20:58:46 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS]" -@@ -23,7 +23,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 |