src/Tools/Code/code_ml.ML
changeset 38863 9070a7c356c9
parent 38784 3b4d63ab03c4
child 38910 6af1d8673cbf
equal deleted inserted replaced
38862:2795499a20bd 38863:9070a7c356c9
   964 
   964 
   965 val setup =
   965 val setup =
   966   Code_Target.add_target
   966   Code_Target.add_target
   967     (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
   967     (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
   968       check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   968       check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   969         make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
   969         make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
   970   #> Code_Target.add_target
   970   #> Code_Target.add_target
   971     (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
   971     (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
   972       check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   972       check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   973         make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
   973         make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
   974   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   974   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   975       brackify_infix (1, R) fxy (
   975       brackify_infix (1, R) fxy (
   976         print_typ (INFX (1, X)) ty1,
   976         print_typ (INFX (1, X)) ty1,
   977         str "->",
   977         str "->",
   978         print_typ (INFX (1, R)) ty2
   978         print_typ (INFX (1, R)) ty2