458 (target, { serializer = serializer, literals = literals, |
458 (target, { serializer = serializer, literals = literals, |
459 check = { env_var = "SCALA_HOME", |
459 check = { env_var = "SCALA_HOME", |
460 make_destination = fn p => Path.append p (Path.explode "ROOT.scala"), |
460 make_destination = fn p => Path.append p (Path.explode "ROOT.scala"), |
461 make_command = fn _ => |
461 make_command = fn _ => |
462 "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"}, |
462 "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"}, |
463 evaluation_args = Token.explode Keyword.empty_keywords @{here} "case_insensitive"}) |
463 evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"}) |
464 #> Code_Target.set_printings (Type_Constructor ("fun", |
464 #> Code_Target.set_printings (Type_Constructor ("fun", |
465 [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
465 [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
466 brackify_infix (1, R) fxy ( |
466 brackify_infix (1, R) fxy ( |
467 print_typ BR ty1 (*product type vs. tupled arguments!*), |
467 print_typ BR ty1 (*product type vs. tupled arguments!*), |
468 str "=>", |
468 str "=>", |