Admin/polyml/settings
changeset 61158 ea6a4c8bc722
parent 61136 168f84f45730
child 61161 8fbab2f3433f
--- a/Admin/polyml/settings	Fri Sep 11 17:48:49 2015 +0200
+++ b/Admin/polyml/settings	Fri Sep 11 17:57:34 2015 +0200
@@ -3,56 +3,67 @@
 POLYML_HOME="$COMPONENT"
 
 
-# simple settings (example)
+# platform preference
 
-#ML_SYSTEM=polyml-5.5.3
-#ML_PLATFORM="$ISABELLE_PLATFORM32"
-#ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-#ML_OPTIONS="-H 500"
-#ML_SOURCES="$POLYML_HOME/src"
-
-
-# smart settings
-
-ML_SYSTEM=polyml-5.5.3
+if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
+then
+  ML_SYSTEM_64="true"
+else
+  ML_SYSTEM_64="false"
+fi
 
-case "$ISABELLE_PLATFORM" in
-  *-linux)
-    if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
-      "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
-    then
-      ML_PLATFORM="$ISABELLE_PLATFORM32"
-    else
-      ML_PLATFORM="$ISABELLE_PLATFORM64"
-      if [ -z "$ML_PLATFORM_FALLBACK" ]; then
-        echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
-        echo >&2 "### Using bulky 64bit version of Poly/ML instead"
-        ML_PLATFORM_FALLBACK="true"
-      fi
-    fi
+case "${ISABELLE_PLATFORM}:${ML_SYSTEM_64}" in
+  x86-cygwin:true)
+    PLATFORMS="x86_64-windows x86-windows"
     ;;
-  x86-cygwin)
-    ML_PLATFORM="x86-windows"
+  x86-cygwin:*)
+    PLATFORMS="x86-windows x86_64-windows"
+    ;;
+  *:true)
+    PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32"
     ;;
   *)
-    ML_PLATFORM="$ISABELLE_PLATFORM32"
+    PLATFORMS="$ISABELLE_PLATFORM32 $ISABELLE_PLATFORM64"
     ;;
 esac
 
-case "$ML_PLATFORM" in
-  x86_64-windows)
-    ML_OPTIONS="-H 1000 --codepage utf8"
-    ;;
-  x86-windows)
-    ML_OPTIONS="-H 500 --codepage utf8"
-    ;;
-  x86_64-*)
-    ML_OPTIONS="-H 1000"
-    ;;
-  *)
-    ML_OPTIONS="-H 500"
-    ;;
-esac
+
+# check executable
+
+unset ML_HOME
+
+for PLATFORM in $PLATFORMS
+do
+  if [ -z "$ML_HOME" ]
+  then
+    if "$POLYML_HOME/$PLATFORM/polyml" -v >/dev/null 2>/dev/null
+    then
+
+      # ML settings
+
+      ML_SYSTEM=polyml-5.5.3
+      ML_PLATFORM="$PLATFORM"
+      ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+      ML_SOURCES="$POLYML_HOME/src"
 
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_SOURCES="$POLYML_HOME/src"
+      case "$ML_PLATFORM" in
+        x86_64-windows)
+          ML_OPTIONS="-H 1000 --codepage utf8"
+          ;;
+        x86-windows)
+          ML_OPTIONS="-H 500 --codepage utf8"
+          ;;
+        x86_64-*)
+          ML_OPTIONS="-H 1000"
+          ;;
+        *)
+          ML_OPTIONS="-H 500"
+          ;;
+      esac
+
+    fi
+  fi
+done
+
+unset PLATFORM
+unset PLATFORMS