more robust: avoid spurious line breaks that might confuse the scala interpreter;
authorwenzelm
Fri, 25 Sep 2020 14:37:07 +0200
changeset 72295 aafec95bc30e
parent 72294 25c6423ec538
child 72296 00490c408e52
more robust: avoid spurious line breaks that might confuse the scala interpreter;
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;