tuned
authorhaftmann
Thu, 27 Dec 2012 21:01:08 +0100
changeset 50627 e91f6c6fb36e
parent 50626 e21485358c56
child 50628 1087c7f1d906
tuned
src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Dec 27 21:01:08 2012 +0100
+++ b/src/Tools/Code/code_printer.ML	Thu Dec 27 21:01:08 2012 +0100
@@ -261,8 +261,7 @@
   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
 
 fun brackify_infix infx fxy_ctxt (l, m, r) =
-  (if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
-    ([l, str " ", m, Pretty.brk 1, r]);
+  gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r];
 
 fun brackify_block fxy_ctxt p1 ps p2 =
   let val p = Pretty.block_enclose (p1, p2) ps
@@ -273,11 +272,10 @@
 
 fun gen_applify strict opn cls f fxy_ctxt p [] =
       if strict
-      then (if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block) [p, str "()"]
+      then gen_brackify (fixity BR fxy_ctxt) [p, str "()"]
       else p
   | gen_applify strict opn cls f fxy_ctxt p ps =
-      (if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block)
-        (p @@ enum "," opn cls (map f ps));
+      gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps));
 
 fun applify opn = gen_applify false opn;