# HG changeset patch
# User wenzelm
# Date 1712332029 -7200
# Node ID 1b986e5f9764a7bef014fdf833e2934cbdb16ef2
# Parent  5c73934777fc76ae4c4a970fc53015871567731d
adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;

diff -r 5c73934777fc -r 1b986e5f9764 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Apr 05 17:10:02 2024 +0200
+++ b/src/Tools/Code/code_scala.ML	Fri Apr 05 17:47:09 2024 +0200
@@ -188,7 +188,7 @@
               in concat [str "case", p_pat, str "=>", p_body] end;
           in
             map print_select clauses
-            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
+            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match {"], str "}")
             |> single
             |> enclose "(" ")"
           end;
@@ -249,7 +249,7 @@
           else
             Pretty.block_enclose
               (concat [head, tuplify (map (str o lookup_var vars2) params),
-                str "match", str "{"], str "}")
+                str "match {"], str "}")
               (map print_clause eqs)
           end;
     val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;