tuned brackets for let expressions etc.

--- a/src/Tools/code/code_haskell.ML	Mon Jun 15 16:13:19 2009 +0200
+++ b/src/Tools/code/code_haskell.ML	Tue Jun 16 14:56:59 2009 +0200
@@ -106,11 +106,9 @@
               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
-          in 
-            Pretty.block_enclose (
-              str "(let {",
-              concat [str "}", str "in", pr_term tyvars thm vars' NOBR body, str ")"]
-            ) ps
+          in brackify_block fxy (str "let {")
+            ps
+            (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body])
           end
       | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
           let
@@ -118,11 +116,10 @@
               let
                 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
-          in
-            Pretty.block_enclose (
-              concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"],
-              str "})"
-            ) (map pr clauses)
+          in brackify_block fxy
+            (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
+            (map pr clauses)
+            (str "}") 
           end
       | pr_case tyvars thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];

--- a/src/Tools/code/code_ml.ML	Mon Jun 15 16:13:19 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Tue Jun 16 14:56:59 2009 +0200
@@ -151,7 +151,7 @@
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
           in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
+            brackets (
               str "case"
               :: pr_term is_closure thm vars NOBR t
               :: pr "of" clause
@@ -441,8 +441,10 @@
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
-            fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
-          in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
+          in
+            brackify_block fxy (Pretty.chunks ps) []
+              (pr_term is_closure thm vars' NOBR body)
+          end
       | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun pr delim (pat, body) =
@@ -450,7 +452,7 @@
                 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
-            (Pretty.enclose "(" ")" o single o brackify fxy) (
+            brackets (
               str "match"
               :: pr_term is_closure thm vars NOBR t
               :: pr "with" clause

--- a/src/Tools/code/code_printer.ML	Mon Jun 15 16:13:19 2009 +0200
+++ b/src/Tools/code/code_printer.ML	Tue Jun 16 14:56:59 2009 +0200
@@ -45,6 +45,7 @@
   val APP: fixity
   val brackify: fixity -> Pretty.T list -> Pretty.T
   val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
+  val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
 
   type itype = Code_Thingol.itype
   type iterm = Code_Thingol.iterm
@@ -175,6 +176,13 @@
 fun brackify_infix infx fxy_ctxt =
   gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
 
+fun brackify_block fxy_ctxt p1 ps p2 =
+  let val p = Pretty.block_enclose (p1, p2) ps
+  in if fixity BR fxy_ctxt
+    then Pretty.enclose "(" ")" [p]
+    else p
+  end;
+
 
 (* generic syntax *)