diff -r 13f4056c42d7 -r ea6a4c8bc722 Admin/polyml/settings --- 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