463 |
463 |
464 val _ = Theory.setup |
464 val _ = Theory.setup |
465 (Code_Target.add_language |
465 (Code_Target.add_language |
466 (target, { serializer = serializer, literals = literals, |
466 (target, { serializer = serializer, literals = literals, |
467 check = { env_var = "SCALA_HOME", |
467 check = { env_var = "SCALA_HOME", |
468 make_destination = fn p => Path.append p (Path.explode "ROOT.scala"), |
468 make_destination = fn p => p + Path.explode "ROOT.scala", |
469 make_command = fn _ => |
469 make_command = fn _ => |
470 "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"}, |
470 "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"}, |
471 evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"}) |
471 evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"}) |
472 #> Code_Target.set_printings (Type_Constructor ("fun", |
472 #> Code_Target.set_printings (Type_Constructor ("fun", |
473 [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
473 [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |