diff options
| author | Edwin Groothuis <edwin@FreeBSD.org> | 2008-08-15 04:33:04 +0000 |
|---|---|---|
| committer | Edwin Groothuis <edwin@FreeBSD.org> | 2008-08-15 04:33:04 +0000 |
| commit | 0002baf18813f5041ee75b5ec58dbe402be8aadc (patch) | |
| tree | 8ef73fea6ccf16a0585301ef5f8f299d4b08b1cc /math/isabelle/files | |
| parent | Forgotten in previous commit. (diff) | |
[MAINTAINER] math/isabelle: update from 2007 to 2008
Updates the port to the latest Isabelle release. It does
not seem worth the effort to continually patch the bash
script files to make them work under sh, hence the large
number of removed files.
PR: ports/126067
Submitted by: Timothy Bourke <timbob@bigpond.com>
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 |