src/Tools/Code/code_ml.ML
changeset 62475 43e64c770f28
parent 61129 774752af4a1f
child 62511 93fa1efc7219
equal deleted inserted replaced
62474:af131b9af420 62475:43e64c770f28
   867   (Code_Target.add_language
   867   (Code_Target.add_language
   868     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   868     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   869       check = { env_var = "ISABELLE_PROCESS",
   869       check = { env_var = "ISABELLE_PROCESS",
   870         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   870         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   871         make_command = fn _ =>
   871         make_command = fn _ =>
   872           "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
   872           "\"$ISABELLE_PROCESS\" -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
   873   #> Code_Target.add_language
   873   #> Code_Target.add_language
   874     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   874     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   875       check = { env_var = "ISABELLE_OCAML",
   875       check = { env_var = "ISABELLE_OCAML",
   876         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   876         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   877         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   877         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })