# HG changeset patch
# User haftmann
# Date 1331320636 -3600
# Node ID 7b04cfc24eb666c1e8e66508b35e9746e805e683
# Parent  13eeb06847cb0188d1582fdf858327777fb0e0a8
always bracket case expressions in Scala

diff -r 13eeb06847cb -r 7b04cfc24eb6 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Mar 09 17:24:42 2012 +0000
+++ b/src/Tools/Code/code_scala.ML	Fri Mar 09 20:17:16 2012 +0100
@@ -130,10 +130,11 @@
                 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
                 val p_body = print_term tyvars false some_thm vars' NOBR body
               in concat [str "case", p_pat, str "=>", p_body] end;
-          in brackify_block fxy
-            (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
-            (map print_select clauses)
-            (str "}")
+          in
+            map print_select clauses
+            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
+            |> single
+            |> enclose "(" ")"
           end
       | print_case tyvars some_thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];