# HG changeset patch
# User haftmann
# Date 1352317684 -3600
# Node ID 286dfcab9833a06fc8c571425f50572af8223273
# Parent  d96a3f46820310942fcbc9c8c317e8ff08470594
restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
restore more conventional namespace during check (relevant for Imperative-HOL)

diff -r d96a3f468203 -r 286dfcab9833 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Nov 06 19:18:35 2012 +0100
+++ b/src/Tools/Code/code_ml.ML	Wed Nov 07 20:48:04 2012 +0100
@@ -832,7 +832,8 @@
     (target_SML, { serializer = serializer_sml, literals = literals_sml,
       check = { env_var = "ISABELLE_PROCESS",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
-        make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
+        make_command = fn _ =>
+          "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => Posix.Process.exit 0w1' Pure" } })
   #> Code_Target.add_target
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "ISABELLE_OCAML",