Update port: math/isabelle

	Update to Isabelle port:
	* Works with updated sml-nj-devel port.
	* Does not require bash
	Thanks to Johannes 5 Joemann for helpful comments/patches.

PR:		ports/116046
Submitted by:	Timothy Bourke <timbob@bigpond.com>

43 files changed, 1103 insertions, 14 deletions

diff --git a/math/isabelle/Makefile b/math/isabelle/Makefile
index 61384f95ae92..7e6bf775bd2d 100644
--- a/math/isabelle/Makefile
+++ b/math/isabelle/Makefile
@@ -7,7 +7,7 @@
 
 PORTNAME=	isabelle
 PORTVERSION=	2005
-PORTREVISION=	1
+PORTREVISION=	2
 CATEGORIES=	math
 MASTER_SITES=	http://isabelle.in.tum.de/dist/ \
 		http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ \
@@ -28,7 +28,7 @@ OPTIONS=	SMLNJ "Use SML/NJ (devel) instead of the faster Poly/ML" Off
 
 .if defined(WITH_SMLNJ)
 ML_SYSTEM=	smlnj-110
-ML_HOME=	${LOCALBASE}/smlnj/bin
+ML_HOME=	${LOCALBASE}/bin
 ML_OPTIONS=	@SMLdebug=/dev/null
 ML_PLATFORM=	x86-bsd
 .else
@@ -40,15 +40,14 @@ ML_PLATFORM=	""
 .endif
 
 USE_PERL5=	yes
-BUILD_DEPENDS+=	bash:${PORTSDIR}/shells/bash
 RUN_DEPENDS+=	proofgeneral:${PORTSDIR}/math/proofgeneral
 
 DOCFILES=	Contents *.pdf *.eps *.ps *.dvi
 
 .if defined(WITH_SMLNJ)
 PLIST_SUB=	HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM}
-BUILD_DEPENDS+=	sml:${PORTSDIR}/lang/sml-nj-devel
-RUN_DEPENDS+=	sml:${PORTSDIR}/lang/sml-nj-devel
+BUILD_DEPENDS+=	smlnj-devel>=110.65:${PORTSDIR}/lang/sml-nj-devel
+MAKE_ENV+=	SMLNJ_DEVEL=yes
 .else
 PLIST_SUB=	HEAPSUBDIR=${ML_SYSTEM}
 BUILD_DEPENDS+=	poly:${PORTSDIR}/lang/polyml
@@ -77,6 +76,8 @@ post-patch:
 		${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings
 	@${RM} ${WRKSRC}/etc/settings.presed
 	@${TOUCH} ${WRKSRC}/contrib/.keep
+	@${REINPLACE_CMD} -e 's|%%SMLNJ_VERSION%%|SMLNJ_DEVEL=yes|' \
+			${WRKSRC}/lib/scripts/run-smlnj
 
 post-install:
 	${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin
diff --git a/math/isabelle/files/Makefile b/math/isabelle/files/Makefile
index 856f2210a630..b81cf2380cff 100644
--- a/math/isabelle/files/Makefile
+++ b/math/isabelle/files/Makefile
@@ -19,10 +19,10 @@ install:
 	for f in ${SRCDIRS}; \
 		do for g in `find -d $$f -type d`; \
 		   do mkdir -p ${DESTDIR}/$$g; \
-		      files=`find $$g -depth 1 -type f \\! -perm +u+x`; \
+  files=`find -E $$g -depth 1 -type f -not -regex '.*\.(bak|orig)$$' -not -perm +u+x`; \
 			    if [ "$$files" != "" ]; then ${BSD_INSTALL_DATA} \
 			$$files ${DESTDIR}/$$g; fi; \
-		      scripts=`find $$g -depth 1 -type f -perm +u+x`; \
+  scripts=`find -E $$g -depth 1 -type f -not -regex '.*\.(bak|orig)$$' -perm +u+x`; \
 		     if [ "$$scripts" != "" ]; then ${BSD_INSTALL_SCRIPT} \
 			$$scripts ${DESTDIR}/$$g; fi; \
 		   done; \
diff --git a/math/isabelle/files/patch-bin-Isabelle b/math/isabelle/files/patch-bin-Isabelle
new file mode 100644
index 000000000000..86b306d14cee
--- /dev/null
+++ b/math/isabelle/files/patch-bin-Isabelle
@@ -0,0 +1,8 @@
+--- ./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
new file mode 100644
index 000000000000..62b441a378bb
--- /dev/null
+++ b/math/isabelle/files/patch-bin-isabelle
@@ -0,0 +1,8 @@
+--- ./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
new file mode 100644
index 000000000000..a8ec33a1f2a3
--- /dev/null
+++ b/math/isabelle/files/patch-bin-isabelle_interface
@@ -0,0 +1,23 @@
+--- ./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
new file mode 100644
index 000000000000..6ea88241f700
--- /dev/null
+++ b/math/isabelle/files/patch-bin-isabelle_process
@@ -0,0 +1,32 @@
+--- ./bin/isabelle-process.orig	Sun Sep  2 15:23:58 2007
++++ ./bin/isabelle-process	Sun Sep  2 16:05:51 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: isabelle-process,v 1.13 2005/07/19 15:21:45 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 [OPTIONS] [INPUT] [OUTPUT]"
+@@ -48,7 +48,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
new file mode 100644
index 000000000000..a536b5cf75ff
--- /dev/null
+++ b/math/isabelle/files/patch-bin-isatool
@@ -0,0 +1,32 @@
+--- ./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
new file mode 100644
index 000000000000..c95bf5db4b84
--- /dev/null
+++ b/math/isabelle/files/patch-build
@@ -0,0 +1,41 @@
+--- build.orig	Mon Sep 26 21:12:24 2005
++++ build	Sun Sep  2 19:02:32 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: build,v 1.35 2005/09/26 11:12:24 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
+@@ -169,7 +169,7 @@
+ 
+ # build it
+ 
+-SECONDS=0
++SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` ))
+ echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+ 
+ for L in $MAKE_LOGICS
diff --git a/math/isabelle/files/patch-lib-Tools-browser b/math/isabelle/files/patch-lib-Tools-browser
new file mode 100644
index 000000000000..c6330107fc80
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-browser
@@ -0,0 +1,26 @@
+--- ./lib/Tools/browser.orig	Sun Sep  2 15:11:55 2007
++++ ./lib/Tools/browser	Sun Sep  2 15:47:49 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: browser,v 1.16 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 [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-convert b/math/isabelle/files/patch-lib-Tools-convert
new file mode 100644
index 000000000000..97a0515e6ee2
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-convert
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..2cff3a23e8a1
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-dimacs2hol
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..cd0f0453d65a
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-display
@@ -0,0 +1,26 @@
+--- ./lib/Tools/display.orig	Sun Sep  2 15:11:55 2007
++++ ./lib/Tools/display	Sun Sep  2 15:48:09 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: display,v 1.8 2005/04/13 16:48:19 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
new file mode 100644
index 000000000000..47790edec2c6
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-doc
@@ -0,0 +1,26 @@
+--- ./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
new file mode 100644
index 000000000000..f2553f4c41ee
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-document
@@ -0,0 +1,44 @@
+--- ./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
new file mode 100644
index 000000000000..d8f622317fa2
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-expandshort
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..32b5c9b89227
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-findlogics
@@ -0,0 +1,17 @@
+--- ./lib/Tools/findlogics.orig	Sun Sep  2 15:11:55 2007
++++ ./lib/Tools/findlogics	Sun Sep  2 15:48:27 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: findlogics,v 1.8 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"
diff --git a/math/isabelle/files/patch-lib-Tools-fixcpure b/math/isabelle/files/patch-lib-Tools-fixcpure
new file mode 100644
index 000000000000..987dee280477
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-fixcpure
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..d182ad0a897e
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-fixgreek
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..a73ea7a9bb17
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-fixheaders
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..6af6a93a2f3e
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-fixsome
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..310071e543ed
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-getenv
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..8c61bcea857e
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-install
@@ -0,0 +1,54 @@
+--- ./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-latex b/math/isabelle/files/patch-lib-Tools-latex
new file mode 100644
index 000000000000..8c4881b113f8
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-latex
@@ -0,0 +1,65 @@
+--- ./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
new file mode 100644
index 000000000000..96d4abb02507
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-logo
@@ -0,0 +1,26 @@
+--- ./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
new file mode 100644
index 000000000000..38124254928e
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-make
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..97bea8bc4bd9
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-makeall
@@ -0,0 +1,28 @@
+--- lib/Tools/makeall.orig	Wed Apr 27 03:50:14 2005
++++ lib/Tools/makeall	Sun Sep  2 19:04:36 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: makeall,v 1.19 2005/04/26 17:50:14 wenzelm Exp $
+ # Author: Markus Wenzel, TU Muenchen
+@@ -13,8 +13,9 @@
+ ## diagnostics
+ 
+ PRG="$(basename "$0")"
++SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` ))
+ 
+-function usage()
++usage()
+ {
+   echo
+   echo "Usage: $PRG [ARGS ...]"
+@@ -24,7 +25,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
new file mode 100644
index 000000000000..16eda28a5716
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-mkdir
@@ -0,0 +1,26 @@
+--- ./lib/Tools/mkdir.orig	Sun Sep  2 15:11:55 2007
++++ ./lib/Tools/mkdir	Sun Sep  2 15:49:15 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: mkdir,v 1.42 2005/06/20 20:13:55 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-print b/math/isabelle/files/patch-lib-Tools-print
new file mode 100644
index 000000000000..b64170ce1ee6
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-print
@@ -0,0 +1,26 @@
+--- ./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
new file mode 100644
index 000000000000..35a0665b887a
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-unsymbolize
@@ -0,0 +1,17 @@
+--- ./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
new file mode 100644
index 000000000000..ac7003db18e0
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-usedir
@@ -0,0 +1,57 @@
+--- lib/Tools/usedir.orig	Wed Aug 31 23:46:31 2005
++++ lib/Tools/usedir	Sun Sep  2 19:04:54 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: usedir,v 1.60 2005/08/31 13:46:31 wenzelm Exp $
+ # Author: Markus Wenzel, TU Muenchen
+@@ -10,7 +10,7 @@
+ 
+ PRG="$(basename "$0")"
+ 
+-function usage()
++usage()
+ {
+   echo
+   echo "Usage: $PRG [OPTIONS] LOGIC NAME"
+@@ -40,18 +40,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\""
+ }
+@@ -77,7 +77,7 @@
+ PROOFS=0
+ VERBOSE=false
+ 
+-function getoptions()
++getoptions()
+ {
+   OPTIND=1
+   while getopts "C:D:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
+@@ -198,7 +198,7 @@
+ fi
+ 
+ 
+-SECONDS=0
++SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` ))
+ 
+ if [ -n "$BUILD" ]; then
+   ITEM="$SESSION"
diff --git a/math/isabelle/files/patch-lib-Tools-version b/math/isabelle/files/patch-lib-Tools-version
new file mode 100644
index 000000000000..37bbbb0fbe54
--- /dev/null
+++ b/math/isabelle/files/patch-lib-Tools-version
@@ -0,0 +1,8 @@
+--- ./lib/Tools/version.orig	Sun Sep  2 15:11:55 2007
++++ ./lib/Tools/version	Sun Sep  2 15:49:33 2007
+@@ -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-feeder b/math/isabelle/files/patch-lib-scripts-feeder
new file mode 100644
index 000000000000..2c0963651e3a
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-feeder
@@ -0,0 +1,26 @@
+--- ./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-getsettings b/math/isabelle/files/patch-lib-scripts-getsettings
new file mode 100644
index 000000000000..fd1dd995c4ec
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-getsettings
@@ -0,0 +1,39 @@
+--- ./lib/scripts/getsettings.orig	Sun Sep  2 15:59:52 2007
++++ ./lib/scripts/getsettings	Sun Sep  2 16:03:07 2007
+@@ -2,7 +2,7 @@
+ # $Id: getsettings,v 1.24 2005/06/06 07:28:28 kleing Exp $
+ # Author: Markus Wenzel, TU Muenchen
+ #
+-# getsettings - bash source script to augment current env.
++# getsettings - sh source script to augment current env.
+ 
+ if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
+ then
+@@ -24,10 +24,9 @@
+ 
+ #users tend to put strange things in here ...
+ unset ENV
+-unset BASH_ENV
+ 
+ #support easy settings
+-function choosefrom ()
++choosefrom ()
+ {
+   local RESULT=""
+   local FILE=""
+@@ -42,13 +41,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; }
+ 
+ #append ML system identifier to paths
+ 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
new file mode 100644
index 000000000000..712f12891bac
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-patch_scripts.bash
@@ -0,0 +1,37 @@
+--- 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
new file mode 100644
index 000000000000..f5c45cbc09b9
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-polyml_platform
@@ -0,0 +1,8 @@
+--- ./lib/scripts/polyml-platform.orig	Sun Sep  2 15:13:40 2007
++++ ./lib/scripts/polyml-platform	Sun Sep  2 15:54:17 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: polyml-platform,v 1.1 2005/08/01 17:20:48 wenzelm Exp $
+ #
diff --git a/math/isabelle/files/patch-lib-scripts-polyml_version b/math/isabelle/files/patch-lib-scripts-polyml_version
new file mode 100644
index 000000000000..f099f97ac77b
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-polyml_version
@@ -0,0 +1,8 @@
+--- ./lib/scripts/polyml-version.orig	Sun Sep  2 15:13:40 2007
++++ ./lib/scripts/polyml-version	Sun Sep  2 15:54:22 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: polyml-version,v 1.2 2005/09/15 15:18:57 wenzelm Exp $
+ #
diff --git a/math/isabelle/files/patch-lib-scripts-run_mosml b/math/isabelle/files/patch-lib-scripts-run_mosml
new file mode 100644
index 000000000000..bc7fa92d97af
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-run_mosml
@@ -0,0 +1,35 @@
+--- 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
new file mode 100644
index 000000000000..c768481055d2
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-run_polyml
@@ -0,0 +1,57 @@
+--- lib/scripts/run-polyml.orig	Tue Aug 16 21:42:17 2005
++++ lib/scripts/run-polyml	Sun Sep  2 17:17:10 2007
+@@ -1,22 +1,36 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: run-polyml,v 1.38 2005/08/16 11:42:17 wenzelm Exp $
+ # Author: Markus Wenzel, TU Muenchen
+ #
+ # Poly/ML startup script.
+ 
+-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
++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"
+ 
+ 
+ ## 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
+@@ -35,11 +49,11 @@
+   *-cygwin)
+     ML_DBASE_SUFFIX=".pmd"
+     POLY="$ML_HOME/PolyML.exe"
+-    function fixpath () { cygpath -m "$@"; }
++    fixpath () { cygpath -m "$@"; }
+     ;;
+   *)
+     POLY="$ML_HOME/poly"
+-    function fixpath () { echo -n "$@"; }
++    fixpath () { echo -n "$@"; }
+     ;;
+ esac
+ 
diff --git a/math/isabelle/files/patch-lib-scripts-run_smlnj b/math/isabelle/files/patch-lib-scripts-run_smlnj
new file mode 100644
index 000000000000..df6762aab7e5
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-run_smlnj
@@ -0,0 +1,68 @@
+--- lib/scripts/run-smlnj.orig	Mon Jun 21 18:25:58 2004
++++ lib/scripts/run-smlnj	Sun Sep  2 20:02:25 2007
+@@ -5,18 +5,16 @@
+ #
+ # SML/NJ startup script (for 110 or later).
+ 
+-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
+ 
+ SML="$ML_HOME/sml"
+-ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
+ 
+ check_mlhome_file "$SML"
+-check_mlhome_file "$ARCH_N_OPSYS"
+ 
+ 
+ 
+@@ -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 @@
+ ## fix heap file name and permissions
+ 
+ if [ -n "$OUTFILE" ]; then
+-  eval $("$ARCH_N_OPSYS")
+-  [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
++  [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ML_PLATFORM"
+   HEAP="$OUTFILE.$HEAP_SUFFIX"
+   check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
+     [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
diff --git a/math/isabelle/files/patch-lib-scripts-showtime b/math/isabelle/files/patch-lib-scripts-showtime
new file mode 100644
index 000000000000..589381f8f1ec
--- /dev/null
+++ b/math/isabelle/files/patch-lib-scripts-showtime
@@ -0,0 +1,26 @@
+--- lib/scripts/showtime.orig	Mon Jun 21 18:25:58 2004
++++ lib/scripts/showtime	Sun Sep  2 19:05:48 2007
+@@ -1,18 +1,18 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: showtime,v 1.5 2004/06/21 08:25:58 kleing Exp $
+ # Author: Markus Wenzel, TU Muenchen
+ #
+ # showtime - print time.
+ 
+-TIME="$1"
++TIME=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` - "$1" ))
+ 
+-SECS=$[ $TIME % 60 ]
++SECS=$(( $TIME % 60 ))
+ [ $SECS -lt 10 ] && SECS="0$SECS"
+ 
+-MINUTES=$[ ($TIME / 60) % 60 ]
++MINUTES=$(( ($TIME / 60) % 60 ))
+ [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
+ 
+-HOURS=$[ $TIME / 3600 ]
++HOURS=$(( $TIME / 3600 ))
+ 
+ echo "${HOURS}:${MINUTES}:${SECS}"
diff --git a/math/isabelle/files/patch-src-Pure-mk b/math/isabelle/files/patch-src-Pure-mk
new file mode 100644
index 000000000000..d4d44b60d4fd
--- /dev/null
+++ b/math/isabelle/files/patch-src-Pure-mk
@@ -0,0 +1,35 @@
+--- src/Pure/mk.orig	Sun Jun 12 07:19:36 2005
++++ src/Pure/mk	Sun Sep  2 19:22:39 2007
+@@ -1,4 +1,4 @@
+-#!/usr/bin/env bash
++#!/bin/sh
+ #
+ # $Id: mk,v 1.27 2005/06/11 21:19:36 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
+@@ -81,7 +81,7 @@
+ 
+ # run isabelle
+ 
+-SECONDS=0
++SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` ))
+ 
+ if [ -z "$RAW" ]; then
+   ITEM="Pure"
diff --git a/math/isabelle/files/run-polyml-5.0 b/math/isabelle/files/run-polyml-5.0
index f4ba8431e1c2..373b632bee89 100644
--- a/math/isabelle/files/run-polyml-5.0
+++ b/math/isabelle/files/run-polyml-5.0
@@ -1,22 +1,20 @@
-#!/usr/bin/env bash
+#!/bin/sh
 #
 # $Id: run-polyml-5.0,v 1.2 2006/12/08 21:18:35 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
@@ -65,7 +63,6 @@ else
   rm -f "${OUTFILE}.o" || fail_out
 fi
 
-
 ## run it!
 
 MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
@@ -77,6 +74,16 @@ else
   FEEDER_OPTS="-q"
 fi
 
+SAVE_INFILE="$INFILE"
+SAVE_OUTFILE="$OUTFILE"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+INFILE="$SAVE_INFILE"
+OUTFILE="$SAVE_OUTFILE"
+MLTEXT="$SAVE_MLTEXT"
+NOWRITE="$SAVE_NOWRITE"
+
 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"
diff --git a/math/isabelle/pkg-plist b/math/isabelle/pkg-plist
index f3988ce6e0e7..6fa5a34b88e6 100644
--- a/math/isabelle/pkg-plist
+++ b/math/isabelle/pkg-plist
@@ -1959,7 +1959,6 @@ bin/isatool
 %%DATADIR%%/etc/isar-keywords.el
 %%DATADIR%%/etc/proofgeneral-settings.el
 %%DATADIR%%/etc/settings
-%%DATADIR%%/etc/settings.orig
 %%DATADIR%%/etc/user-settings.sample
 %%DATADIR%%/heaps/%%HEAPSUBDIR%%/CCL
 %%DATADIR%%/heaps/%%HEAPSUBDIR%%/CTT