# HG changeset patch
# User wenzelm
# Date 1289856678 -3600
# Node ID 1e218365a20e0edf9e56dee103234ca2a2254ed4
# Parent  bbcb7aa90afc7530392be2d69afb7dc883571f67# Parent  5534b18bce5d054765a644926f10c419f77f325a
merged

diff -r bbcb7aa90afc -r 1e218365a20e etc/settings
--- a/etc/settings	Mon Nov 15 22:24:08 2010 +0100
+++ b/etc/settings	Mon Nov 15 22:31:18 2010 +0100
@@ -18,13 +18,13 @@
 # Poly/ML 5.x (automated settings)
 POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
 ML_PLATFORM="$ISABELLE_PLATFORM"
-ML_HOME=$(choosefrom \
+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" \
-  $POLY_HOME)
+  "$POLY_HOME")"
 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
 ML_OPTIONS="-H 200"
 ML_SOURCES="$ML_HOME/../src"
@@ -170,13 +170,13 @@
 ###
 
 # Proof General home, look in a variety of places
-PROOFGENERAL_HOME=$(choosefrom \
+PROOFGENERAL_HOME="$(choosefrom \
   "$ISABELLE_HOME/contrib/ProofGeneral" \
   "$ISABELLE_HOME/../ProofGeneral" \
   "/usr/local/ProofGeneral" \
   "/usr/share/ProofGeneral" \
   "/opt/ProofGeneral" \
-  "")
+  "")"
 
 PROOFGENERAL_OPTIONS=""
 #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
diff -r bbcb7aa90afc -r 1e218365a20e lib/scripts/polyml-version
--- a/lib/scripts/polyml-version	Mon Nov 15 22:24:08 2010 +0100
+++ b/lib/scripts/polyml-version	Mon Nov 15 22:31:18 2010 +0100
@@ -2,11 +2,17 @@
 #
 # polyml-version --- determine Poly/ML runtime system version
 
-echo -n polyml
-
 if [ -x "$ML_HOME/poly" ]; then
-  env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
+  VERSION="$(env \
+    LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
     DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
-    "$ML_HOME/poly" -v -H 10 | \
-    sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
+    "$ML_HOME/poly" -v -H 10)"
+  REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$'
+  if [[ "$VERSION" =~ $REGEXP ]]; then
+    echo "polyml${BASH_REMATCH[1]}"
+  else
+    echo polyml-unknown
+  fi
+else
+  echo polyml-unknown
 fi
diff -r bbcb7aa90afc -r 1e218365a20e lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Nov 15 22:24:08 2010 +0100
+++ b/lib/scripts/run-polyml	Mon Nov 15 22:31:18 2010 +0100
@@ -9,24 +9,27 @@
 
 ## diagnostics
 
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
 function fail_out()
 {
-  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
-  exit 2
+  fail "Unable to create output heap file: \"$OUTFILE\""
 }
 
 function check_file()
 {
-  if [ ! -f "$1" ]; then
-    echo "Unable to locate $1" >&2
-    echo "Please check your ML system settings!" >&2
-    exit 2
-  fi
+  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
 }
 
 
 ## compiler executables and libraries
 
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
 POLY="$ML_HOME/poly"
 check_file "$POLY"
 
diff -r bbcb7aa90afc -r 1e218365a20e lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Mon Nov 15 22:24:08 2010 +0100
+++ b/lib/scripts/run-smlnj	Mon Nov 15 22:31:18 2010 +0100
@@ -9,19 +9,20 @@
 
 ## diagnostics
 
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
 function fail_out()
 {
-  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
-  exit 2
+  fail "Unable to create output heap file: \"$OUTFILE\""
 }
 
 function check_mlhome_file()
 {
-  if [ ! -f "$1" ]; then
-    echo "Unable to locate $1" >&2
-    echo "Please check your ML_HOME setting!" >&2
-    exit 2
-  fi
+  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
 }
 
 function check_heap_file()
@@ -38,6 +39,8 @@
 
 ## compiler binaries
 
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
 SML="$ML_HOME/sml"
 ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
 
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/BV/BVNoTypeError.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/BV/EffectMono.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/Comp/AuxLemmas.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/Comp/LemmasComp.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/Comp/NatCanonify.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/DFA/Abstract_BV.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/DFA/LBVCorrect.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/DFA/Semilattices.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/J/Example.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/J/JTypeSafe.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/J/Term.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/J/Type.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/JVM/JVMInstructions.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/MicroJava.thy
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/ROOT.ML
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/document/introduction.tex
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/document/root.bib
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/MicroJava/document/root.tex
diff -r bbcb7aa90afc -r 1e218365a20e src/HOL/Tools/Predicate_Compile/etc/settings
--- a/src/HOL/Tools/Predicate_Compile/etc/settings	Mon Nov 15 22:24:08 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings	Mon Nov 15 22:31:18 2010 +0100
@@ -1,16 +1,17 @@
+# -*- shell-script -*- :mode=shellscript:
 
-EXEC_SWIPL=$(choosefrom \
+EXEC_SWIPL="$(choosefrom \
   "$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \
   "$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \
   "$ISABELLE_HOME/../swipl" \
   $(type -p swipl) \
-  "")
+  "")"
 
-EXEC_YAP=$(choosefrom \
+EXEC_YAP="$(choosefrom \
   "$ISABELLE_HOME/contrib/yap/$ISABELLE_PLATFORM/bin/yap" \
   "$ISABELLE_HOME/contrib_devel/yap/$ISABELLE_PLATFORM/bin/yap" \
   "$ISABELLE_HOME/../yap" \
   $(type -p yap) \
-  "")
+  "")"
 
 SWIPL_VERSION=$("$COMPONENT/lib/scripts/swipl_version")
diff -r bbcb7aa90afc -r 1e218365a20e src/Tools/Code/etc/settings
--- a/src/Tools/Code/etc/settings	Mon Nov 15 22:24:08 2010 +0100
+++ b/src/Tools/Code/etc/settings	Mon Nov 15 22:31:18 2010 +0100
@@ -1,14 +1,15 @@
+# -*- shell-script -*- :mode=shellscript:
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
 
-EXEC_GHC=$(choosefrom \
+EXEC_GHC="$(choosefrom \
   "$ISABELLE_HOME/contrib/ghc/$ISABELLE_PLATFORM/ghc" \
   "$ISABELLE_HOME/../ghc/$ISABELLE_PLATFORM/ghc" \
-  $(type -p ghc) \
-  "")
+  "$(type -p ghc)" \
+  "")"
 
-EXEC_OCAML=$(choosefrom \
+EXEC_OCAML="$(choosefrom \
   "$ISABELLE_HOME/contrib/ocaml/$ISABELLE_PLATFORM/ocaml" \
   "$ISABELLE_HOME/../ocaml/$ISABELLE_PLATFORM/ocaml" \
-  $(type -p ocaml) \
-  "")
+  "$(type -p ocaml)" \
+  "")"