more correct precedence of do-notation
authorhaftmann
Thu, 25 Sep 2014 18:47:32 +0200
changeset 58454 271829a473ed
parent 58453 75b92e25f59f
child 58455 126c353540fc
more correct precedence of do-notation
src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Sep 25 17:07:44 2014 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 25 18:47:32 2014 +0200
@@ -471,8 +471,9 @@
           val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
             (bind :: binds) vars;
         in
-          (brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
+          brackify_block fxy (str "do { ")
             (ps @| print_term vars' NOBR t'')
+            (str " }")
         end
       | NONE => brackify_infix (1, L) fxy
           (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)