# HG changeset patch
# User wenzelm
# Date 1346264182 -7200
# Node ID 0cebcbeac4c7a01a27b436cdd85caa2adf0c2ced
# Parent  3bdebf6ad9dabe483a70e8537b357811137aab80
provide polyml-5.4.1 as regular component;
discontinued old-style choosefrom settings with hardwired defaults;

diff -r 3bdebf6ad9da -r 0cebcbeac4c7 Admin/component_repository/components.sha1
--- a/Admin/component_repository/components.sha1	Wed Aug 29 17:19:48 2012 +0200
+++ b/Admin/component_repository/components.sha1	Wed Aug 29 20:16:22 2012 +0200
@@ -12,6 +12,7 @@
 6425f622625024c1de27f3730d6811f6370a19cd  jedit_build-20120414.tar.gz
 7b012f725ec1cc102dc259df178d511cc7890bba  jedit_build-20120813.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
+1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb  polyml-5.4.1.tar.gz
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
 b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
diff -r 3bdebf6ad9da -r 0cebcbeac4c7 Admin/components/main
--- a/Admin/components/main	Wed Aug 29 17:19:48 2012 +0200
+++ b/Admin/components/main	Wed Aug 29 20:16:22 2012 +0200
@@ -4,6 +4,7 @@
 jdk-7u6
 jedit_build-20120813
 kodkodi-1.2.16
+polyml-5.4.1
 scala-2.9.2
 spass-3.8ds
 z3-4.0
diff -r 3bdebf6ad9da -r 0cebcbeac4c7 Admin/polyml/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/settings	Wed Aug 29 20:16:22 2012 +0200
@@ -0,0 +1,43 @@
+# -*- shell-script -*- :mode=shellscript:
+
+# basic settings
+
+#ML_SYSTEM=polyml-5.4.1
+#ML_PLATFORM="$ISABELLE_PLATFORM"
+#ML_HOME="$COMPONENT/$ML_PLATFORM"
+#ML_OPTIONS="-H 500"
+#ML_SOURCES="$ML_HOME/../src"
+
+
+# smart settings
+
+ML_SYSTEM=polyml-5.4.1
+
+case "$ISABELLE_PLATFORM" in
+  *-linux)
+    if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
+      "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
+    then
+      ML_PLATFORM="$ISABELLE_PLATFORM32"
+    else
+      echo >&2 "### Cannot execute Poly/ML in 32bit mode -- using bulky 64bit version instead"
+      ML_PLATFORM="$ISABELLE_PLATFORM64"
+    fi
+    ;;
+  *)
+    ML_PLATFORM="$ISABELLE_PLATFORM32"
+    ;;
+esac
+
+case "$ML_PLATFORM" in
+  x86_64-*)
+    ML_OPTIONS="-H 1000"
+    ;;
+  *)
+    ML_OPTIONS="-H 500"
+    ;;
+esac
+
+ML_HOME="$COMPONENT/$ML_PLATFORM"
+ML_SOURCES="$COMPONENT/src"
+
diff -r 3bdebf6ad9da -r 0cebcbeac4c7 NEWS
--- a/NEWS	Wed Aug 29 17:19:48 2012 +0200
+++ b/NEWS	Wed Aug 29 20:16:22 2012 +0200
@@ -97,6 +97,10 @@
 
 *** System ***
 
+* The ML system is configured as regular component, and no longer
+picked up from some surrounding directory.  Potential INCOMPATIBILITY
+for home-made configurations.
+
 * The "isabelle logo" tool allows to specify EPS or PDF format; the
 latter is preferred now.  Minor INCOMPATIBILITY.
 
diff -r 3bdebf6ad9da -r 0cebcbeac4c7 etc/settings
--- a/etc/settings	Wed Aug 29 17:19:48 2012 +0200
+++ b/etc/settings	Wed Aug 29 20:16:22 2012 +0200
@@ -8,49 +8,6 @@
 #   * DO NOT COPY this file into your ~/.isabelle directory!
 
 ###
-### ML compiler settings (ESSENTIAL!)
-###
-
-# ML_HOME specifies the location of the actual compiler binaries.  Do
-# not invent new ML system names unless you know what you are doing.
-# Only one of the sections below should be activated.
-
-# Poly/ML default (automated settings)
-ML_PLATFORM="$ISABELLE_PLATFORM"
-ML_HOME="$(choosefrom \
-  "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
-  "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
-  "/usr/local/polyml/$ML_PLATFORM" \
-  "/usr/share/polyml/$ML_PLATFORM" \
-  "/opt/polyml/$ML_PLATFORM" \
-  "")"
-ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
-ML_OPTIONS="-H 200"
-ML_SOURCES="$ML_HOME/../src"
-
-# Poly/ML 32 bit (manual settings)
-#ML_SYSTEM=polyml-5.4.1
-#ML_PLATFORM="$ISABELLE_PLATFORM"
-#ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
-#ML_OPTIONS="-H 500"
-#ML_SOURCES="$ML_HOME/../src"
-
-# Poly/ML 64 bit (manual settings)
-#ML_SYSTEM=polyml-5.4.1
-#ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
-#ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
-#ML_OPTIONS="-H 1000"
-#ML_SOURCES="$ML_HOME/../src"
-
-# Standard ML of New Jersey (slow!)
-#ML_SYSTEM=smlnj-110
-#ML_HOME="/usr/local/smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-#SMLNJ_CYGWIN_RUNTIME=1
-
-
-###
 ### JVM components (Scala or Java)
 ###
 
@@ -175,9 +132,16 @@
 
 
 ###
-### Old-style settings for some external tools
+### Misc old-style settings
 ###
 
+# Standard ML of New Jersey (slow!)
+#ML_SYSTEM=smlnj-110
+#ML_HOME="/usr/local/smlnj/bin"
+#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
+#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
+#SMLNJ_CYGWIN_RUNTIME=1
+
 ## Set HOME only for tools you have installed!
 
 # SVC (Stanford Validity Checker)
diff -r 3bdebf6ad9da -r 0cebcbeac4c7 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Aug 29 17:19:48 2012 +0200
+++ b/lib/scripts/getsettings	Wed Aug 29 20:16:22 2012 +0200
@@ -59,21 +59,6 @@
 unset ENV
 unset BASH_ENV
 
-#support easy settings
-function choosefrom ()
-{
-  local RESULT=""
-  local FILE=""
-
-  for FILE in "$@"
-  do
-    [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
-  done
-
-  [ -z "$RESULT" ] && RESULT="$FILE"
-  echo "$RESULT"
-}
-
 #shared library convenience
 function librarypath () {
   for X in "$@"