more robust: avoid spurious line breaks that might confuse the scala interpreter;
--- a/src/Tools/Code/code_scala.ML Fri Sep 25 13:28:28 2020 +0200
+++ b/src/Tools/Code/code_scala.ML Fri Sep 25 14:37:07 2020 +0200
@@ -287,7 +287,7 @@
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
+ (str ("final case class " ^ deresolve_const co)) vs_args)
@@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
(Name.invent_names (snd reserved) "a" tys))),
str "extends",
@@ -296,7 +296,7 @@
];
in
Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
+ NOBR (str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
:: map print_co cos)
end
| print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) =
@@ -334,7 +334,7 @@
(map print_classparam_val classparams))
:: map print_classparam_def classparams
@| Pretty.block_enclose
- ((concat o map str) ["object", deresolve_class class, "{"], str "}")
+ (str ("object " ^ deresolve_class class ^ "{"), str "}")
(map (print_inst class) insts)
)
end;