src/Tools/Code/code_ml.ML
changeset 62588 cd266473b81b
parent 62579 bfa38c2e751f
child 62634 aa3b47b32100
equal deleted inserted replaced
62587:e31bf8ed5397 62588:cd266473b81b
   866   );
   866   );
   867 
   867 
   868 val _ = Theory.setup
   868 val _ = Theory.setup
   869   (Code_Target.add_language
   869   (Code_Target.add_language
   870     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   870     (target_SML, { serializer = serializer_sml, literals = literals_sml,
   871       check = { env_var = "ISABELLE_PROCESS",
   871       check = { env_var = "ISABELLE_TOOL",
   872         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   872         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   873         make_command = fn _ =>
   873         make_command = fn _ =>
   874           "\"$ISABELLE_PROCESS\" -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
   874           "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
   875   #> Code_Target.add_language
   875   #> Code_Target.add_language
   876     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   876     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   877       check = { env_var = "ISABELLE_OCAML",
   877       check = { env_var = "ISABELLE_OCAML",
   878         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   878         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   879         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   879         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })