src/Tools/Code/code_ml.ML
changeset 41952 c7297638599b
parent 41940 a3b68a7a0e15
child 42599 1a82b0400b2a
equal deleted inserted replaced
41951:117eb7aeddf0 41952:c7297638599b
   839       check = { env_var = "ISABELLE_PROCESS",
   839       check = { env_var = "ISABELLE_PROCESS",
   840         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   840         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   841         make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
   841         make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -u Pure" } })
   842   #> Code_Target.add_target
   842   #> Code_Target.add_target
   843     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   843     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   844       check = { env_var = "EXEC_OCAML",
   844       check = { env_var = "ISABELLE_OCAML",
   845         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   845         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   846         make_command = fn _ => "\"$EXEC_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   846         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   847   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   847   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   848       brackify_infix (1, R) fxy (
   848       brackify_infix (1, R) fxy (
   849         print_typ (INFX (1, X)) ty1,
   849         print_typ (INFX (1, X)) ty1,
   850         str "->",
   850         str "->",
   851         print_typ (INFX (1, R)) ty2
   851         print_typ (INFX (1, R)) ty2