858 print_typ (INFX (1, X)) ty1, |
857 print_typ (INFX (1, X)) ty1, |
859 str "->", |
858 str "->", |
860 print_typ (INFX (1, R)) ty2 |
859 print_typ (INFX (1, R)) ty2 |
861 ); |
860 ); |
862 |
861 |
863 val setup = |
862 val _ = Theory.setup |
864 Code_Target.add_language |
863 (Code_Target.add_language |
865 (target_SML, { serializer = serializer_sml, literals = literals_sml, |
864 (target_SML, { serializer = serializer_sml, literals = literals_sml, |
866 check = { env_var = "ISABELLE_PROCESS", |
865 check = { env_var = "ISABELLE_PROCESS", |
867 make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), |
866 make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), |
868 make_command = fn _ => |
867 make_command = fn _ => |
869 "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } }) |
868 "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } }) |
885 "in", "include", "inherit", "initializer", "lazy", "let", "match", "method", |
884 "in", "include", "inherit", "initializer", "lazy", "let", "match", "method", |
886 "module", "mutable", "new", "object", "of", "open", "or", "private", "rec", |
885 "module", "mutable", "new", "object", "of", "open", "or", "private", "rec", |
887 "sig", "struct", "then", "to", "true", "try", "type", "val", |
886 "sig", "struct", "then", "to", "true", "try", "type", "val", |
888 "virtual", "when", "while", "with" |
887 "virtual", "when", "while", "with" |
889 ] |
888 ] |
890 #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]; |
889 #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]); |
891 |
890 |
892 end; (*struct*) |
891 end; (*struct*) |