src/Tools/Code/code_ml.ML
changeset 41940 a3b68a7a0e15
parent 41343 71f4f15258a5
child 41952 c7297638599b
     1.1 --- a/src/Tools/Code/code_ml.ML	Sun Mar 13 13:57:20 2011 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sun Mar 13 14:51:38 2011 +0100
     1.3 @@ -836,12 +836,14 @@
     1.4  val setup =
     1.5    Code_Target.add_target
     1.6      (target_SML, { serializer = serializer_sml, literals = literals_sml,
     1.7 -      check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
     1.8 -        make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
     1.9 +      check = { env_var = "ISABELLE_PROCESS",
    1.10 +        make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
    1.11 +        make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
    1.12    #> Code_Target.add_target
    1.13      (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
    1.14 -      check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    1.15 -        make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
    1.16 +      check = { env_var = "EXEC_OCAML",
    1.17 +        make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    1.18 +        make_command = fn _ => "\"$EXEC_OCAML\" -w pu nums.cma ROOT.ocaml" } })
    1.19    #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.20        brackify_infix (1, R) fxy (
    1.21          print_typ (INFX (1, X)) ty1,