restored SML code check which got unintentionally broken: must explicitly check for error during compilation;
authorhaftmann
Wed Nov 07 20:48:04 2012 +0100 (2012-11-07)
changeset 50022286dfcab9833
parent 50021 d96a3f468203
child 50023 28f3263d4d1b
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)
src/Tools/Code/code_ml.ML
     1.1 --- a/src/Tools/Code/code_ml.ML	Tue Nov 06 19:18:35 2012 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Wed Nov 07 20:48:04 2012 +0100
     1.3 @@ -832,7 +832,8 @@
     1.4      (target_SML, { serializer = serializer_sml, literals = literals_sml,
     1.5        check = { env_var = "ISABELLE_PROCESS",
     1.6          make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
     1.7 -        make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
     1.8 +        make_command = fn _ =>
     1.9 +          "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => Posix.Process.exit 0w1' Pure" } })
    1.10    #> Code_Target.add_target
    1.11      (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
    1.12        check = { env_var = "ISABELLE_OCAML",