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;