9 files changed, 134 insertions, 74 deletions

diff --git a/math/isabelle/Makefile b/math/isabelle/Makefile
index 69039d169ecb..ae74eda7f151 100644
--- a/math/isabelle/Makefile
+++ b/math/isabelle/Makefile
@@ -22,7 +22,6 @@ MAINTAINER=	timbob@bigpond.com
 COMMENT=	A generic proof assistant
 
 OPTIONS=	SMLNJ "Use SML/NJ (devel) instead of the faster Poly/ML" Off
-NO_PACKAGE=	Requires non-standard kernel setting.
 
 .include <bsd.port.pre.mk>
 
@@ -30,11 +29,13 @@ NO_PACKAGE=	Requires non-standard kernel setting.
 ML_SYSTEM=	smlnj-110
 ML_HOME=	${LOCALBASE}/smlnj/bin
 ML_OPTIONS=	@SMLdebug=/dev/null
+ML_PLATFORM=	x86-bsd
 .else
-ML_SYSTEM=	polyml-4.2.0
-ML_HOME=	${LOCALBASE}/lib/polyml/
-ML_OPTIONS=	-H 80
+ML_SYSTEM=	polyml-5.0
+ML_HOME=	${LOCALBASE}/bin
+ML_OPTIONS=	-H 500
 ML_DBASE=	""
+ML_PLATFORM=	""
 .endif
 
 USE_PERL5=	yes
@@ -43,12 +44,12 @@ RUN_DEPENDS+=	proofgeneral:${PORTSDIR}/math/proofgeneral
 
 DOCFILES=	Contents *.pdf *.eps *.ps *.dvi
 
-PLIST_SUB=	HEAPSUBDIR=${ML_SYSTEM}_x86-bsd
-
 .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
 .else
+PLIST_SUB=	HEAPSUBDIR=${ML_SYSTEM}
 BUILD_DEPENDS+=	poly:${PORTSDIR}/lang/polyml
 RUN_DEPENDS+=	poly:${PORTSDIR}/lang/polyml
 .endif
@@ -57,8 +58,12 @@ NO_INSTALL_MANPAGES=yes
 
 post-extract:
 	@${CP} ${FILESDIR}/Makefile ${WRKSRC}
-	@${CP} ${FILESDIR}/polyml-4.1.4-patch.ML ${WRKSRC}/src/Pure/ML-Systems/
-	@${CP} ${FILESDIR}/polyml-4.2.0.ML ${WRKSRC}/src/Pure/ML-Systems/
+	@${CP} ${FILESDIR}/run-polyml-5.0 ${WRKSRC}/lib/scripts/
+	@${CHMOD} ugo+x ${WRKSRC}/lib/scripts/run-polyml-5.0
+	@${CP} ${FILESDIR}/polyml-5.0.ML ${WRKSRC}/src/Pure/ML-Systems/
+.if !defined(WITH_SMLNJ)
+	@${CP} ${FILESDIR}/proofgeneral-settings.el ${WRKSRC}/etc/
+.endif
 
 post-patch:
 	@${MV} ${WRKSRC}/etc/settings ${WRKSRC}/etc/settings.presed
@@ -66,19 +71,12 @@ post-patch:
 		 s|%%ML_HOME%%|${ML_HOME}|;		\
 		 s|%%ML_OPTIONS%%|\"${ML_OPTIONS}\"|;	\
 		 s|%%ML_DBASE%%|${ML_DBASE}|;		\
+		 s|%%ML_PLATFORM%%|${ML_PLATFORM}|;	\
 		 s|%%PREFIX%%|${PREFIX}|"		\
 		${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings
 	@${RM} ${WRKSRC}/etc/settings.presed
 	@${TOUCH} ${WRKSRC}/contrib/.keep
 
-pre-build:
-.if !defined(WITH_SMLNJ)
-	@if ${TEST} `ulimit -Hd` -lt 917504; then	\
-		${CAT} ${FILESDIR}/badmaxdsiz;		\
-		exit 1;					\
-	fi
-.endif
-
 post-install:
 	${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin
 .if !defined(NOPORTDOCS)
diff --git a/math/isabelle/files/badmaxdsiz b/math/isabelle/files/badmaxdsiz
deleted file mode 100644
index 578ab37d768f..000000000000
--- a/math/isabelle/files/badmaxdsiz
+++ /dev/null
@@ -1,18 +0,0 @@
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-! The system process data segment value is too low!                  !
-!                                                                    !
-! Under these circumstances the Isabelle build process for logics    !
-! such as HOL will not terminate, or otherwise fail.                 !
-!                                                                    !
-! The setting may be viewed and modified with the commands:          !
-!   sh:  ulimit -Hd                                                  !
-!   csh: limit -h datasize                                           !
-!                                                                    !
-! It may be necessary to lift the maximum limit. One way of doing    !
-! this is to add a line to /boot/loader.conf and then to restart the !
-! system:                                                            !
-!    kern.maxdsiz="896M"                                             !
-!                                                                    !
-! This problem only affects Poly/ML. Isabelle may also be configured !
-! to use SML/NJ (build with WITH_SMLNJ=yes).                         !
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
diff --git a/math/isabelle/files/patch-etc-settings b/math/isabelle/files/patch-etc-settings
index 7fa19cbfcb4e..07944e074d80 100644
--- a/math/isabelle/files/patch-etc-settings
+++ b/math/isabelle/files/patch-etc-settings
@@ -34,7 +34,7 @@
 +ML_SYSTEM=%%ML_SYSTEM%%
 +ML_HOME=%%ML_HOME%%
 +ML_OPTIONS=%%ML_OPTIONS%%
-+ML_PLATFORM=x86-bsd
++ML_PLATFORM=%%ML_PLATFORM%%
 +ML_DBASE=%%ML_DBASE%%
  
  ###
diff --git a/math/isabelle/files/polyml-4.2.0.ML b/math/isabelle/files/polyml-4.2.0.ML
deleted file mode 100644
index 20f0eb472278..000000000000
--- a/math/isabelle/files/polyml-4.2.0.ML
+++ /dev/null
@@ -1,9 +0,0 @@
-(*  Title:      Pure/ML-Systems/polyml-4.2.0.ML
-    ID:         $Id: polyml-4.2.0.ML,v 1.1 2005/11/14 13:36:46 wenzelm Exp $
-    Author:     Makarius
-
-Compatibility wrapper for Poly/ML 4.2.0.
-*)
-
-use "ML-Systems/polyml-4.1.4-patch.ML";
-use "ML-Systems/polyml.ML";
diff --git a/math/isabelle/files/polyml-4.1.4-patch.ML b/math/isabelle/files/polyml-5.0.ML
index 196d23b7fda8..94eb9a073c3d 100644
--- a/math/isabelle/files/polyml-4.1.4-patch.ML
+++ b/math/isabelle/files/polyml-5.0.ML
@@ -1,9 +1,7 @@
-(*  Title:      Pure/ML-Systems/polyml-4.1.4-patch.ML
-    ID:         $Id$
-    Author:     Makarius
+(*  Title:      Pure/ML-Systems/polyml-5.0.ML
+    ID:         $Id: polyml-5.0.ML,v 1.1 2006/12/07 13:11:39 wenzelm Exp $
 
-Patch for PolyML 4.1.4 to make it work with Isabelle2005.  We commit
-this into ML_dbase!
+Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005.
 *)
 
 structure Posix =
@@ -29,3 +27,7 @@ struct
   val all = full;
 end;
 
+
+use "ML-Systems/polyml.ML";
+
+val pointer_eq = PolyML.pointerEq;
diff --git a/math/isabelle/files/proofgeneral-settings.el b/math/isabelle/files/proofgeneral-settings.el
new file mode 100644
index 000000000000..c0a74afebada
--- /dev/null
+++ b/math/isabelle/files/proofgeneral-settings.el
@@ -0,0 +1,17 @@
+;;;
+;;; $Id: proofgeneral-settings.el,v 1.2 2001/09/28 18:08:05 wenzelm Exp $
+;;;
+;;; Options for Proof General
+
+;; Examples for sensible settings:
+
+;(custom-set-variables '(isar-eta-contract nil))
+
+;(custom-set-faces
+; '(proof-locked-face
+;   ((((type x) (class color) (background light)) (:background "lightsteelblue2")))))
+
+; Makarius' Poly/ML 5.0 patches
+(custom-set-variables
+ '(proof-shell-pre-interrupt-hook (lambda () t)))
+
diff --git a/math/isabelle/files/run-polyml-5.0 b/math/isabelle/files/run-polyml-5.0
new file mode 100644
index 000000000000..f4ba8431e1c2
--- /dev/null
+++ b/math/isabelle/files/run-polyml-5.0
@@ -0,0 +1,93 @@
+#!/usr/bin/env bash
+#
+# $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()
+{
+  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
+  exit 2
+}
+
+function check_file()
+{
+  if [ ! -f "$1" ]; then
+    echo "Unable to locate $1" >&2
+    echo "Please check your ML system settings!" >&2
+    exit 2
+  fi
+}
+
+
+## compiler executables and libraries
+
+POLY="$ML_HOME/poly"
+check_file "$POLY"
+
+if [ "$(basename "$ML_HOME")" = bin ]; then
+  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
+else
+  POLYLIB="$ML_HOME"
+fi
+
+export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
+export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
+
+
+## prepare databases
+
+if [ -z "$INFILE" ]; then
+  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
+else
+  check_file "$INFILE"
+  POLY="$INFILE"
+  EXIT=""
+fi
+
+ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
+
+if [ -z "$OUTFILE" ]; then
+  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
+else
+  if [ -z "$COMPRESS" ]; then
+    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
+  else
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
+  fi
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+  rm -f "${OUTFILE}.o" || fail_out
+fi
+
+
+## run it!
+
+MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
+MLEXIT="commit();"
+
+if [ -z "$TERMINATE" ]; then
+  FEEDER_OPTS=""
+else
+  FEEDER_OPTS="-q"
+fi
+
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
+
+if [ -n "$OUTFILE" ]; then
+  if [ -e "${OUTFILE}.o" ]; then
+    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
+    rm -f "${OUTFILE}.o"
+    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
+  fi
+  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+fi
+
+exit "$RC"
diff --git a/math/isabelle/pkg-install b/math/isabelle/pkg-install
deleted file mode 100644
index 96d34565e7aa..000000000000
--- a/math/isabelle/pkg-install
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/bin/sh
-
-if [ "$2" = "POST-INSTALL" ]; then
-	if test `ulimit -Hd` -lt 917504; then
-		cat <<END
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-! The system process data segment value is too low!                  !
-!                                                                    !
-! Under these circumstances Isabelle may not function reliably, or   !
-! may fail completely.                                               !
-!                                                                    !
-! The setting may be viewed and modified with the commands:          !
-!   sh:  ulimit -Hd                                                  !
-!   csh: limit -h datasize                                           !
-!                                                                    !
-! It may be necessary to lift the maximum limit. One way of doing    !
-! this is to add a line to /boot/loader.conf and then to restart the !
-! system:                                                            !
-!    kern.maxdsiz="896M"                                             !
-!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
-END
-	fi
-fi
diff --git a/math/isabelle/pkg-plist b/math/isabelle/pkg-plist
index af1336f9ccf3..f3988ce6e0e7 100644
--- a/math/isabelle/pkg-plist
+++ b/math/isabelle/pkg-plist
@@ -2070,6 +2070,7 @@ bin/isatool
 %%DATADIR%%/lib/scripts/polyml-version
 %%DATADIR%%/lib/scripts/run-mosml
 %%DATADIR%%/lib/scripts/run-polyml
+%%DATADIR%%/lib/scripts/run-polyml-5.0
 %%DATADIR%%/lib/scripts/run-smlnj
 %%DATADIR%%/lib/scripts/showtime
 %%DATADIR%%/lib/scripts/unsymbolize.pl
@@ -3341,8 +3342,7 @@ bin/isatool
 %%DATADIR%%/src/Pure/ML-Systems/cpu-timer-basis.ML
 %%DATADIR%%/src/Pure/ML-Systems/cpu-timer-gc.ML
 %%DATADIR%%/src/Pure/ML-Systems/mosml.ML
-%%DATADIR%%/src/Pure/ML-Systems/polyml-4.1.4-patch.ML
-%%DATADIR%%/src/Pure/ML-Systems/polyml-4.2.0.ML
+%%DATADIR%%/src/Pure/ML-Systems/polyml-5.0.ML
 %%DATADIR%%/src/Pure/ML-Systems/polyml-posix.ML
 %%DATADIR%%/src/Pure/ML-Systems/polyml-time-limit.ML
 %%DATADIR%%/src/Pure/ML-Systems/polyml.ML