# HG changeset patch
# User wenzelm
# Date 1601037427 -7200
# Node ID aafec95bc30e792064131cd81af65e7ae77afe7c
# Parent  25c6423ec538fe9760604c179e6bb4b036f280b0
more robust: avoid spurious line breaks that might confuse the scala interpreter;

diff -r 25c6423ec538 -r aafec95bc30e src/Tools/Code/code_scala.ML
--- 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;