# HG changeset patch
# User haftmann
# Date 1262610597 -3600
# Node ID d2803c7f6d5245b27bb02554888df25861979cd5
# Parent  5eaff81220a91877e8dfc049d5ec4baea27aa746
added applify combinator

diff -r 5eaff81220a9 -r d2803c7f6d52 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Mon Jan 04 14:09:57 2010 +0100
+++ b/src/Tools/Code/code_printer.ML	Mon Jan 04 14:09:57 2010 +0100
@@ -60,6 +60,7 @@
   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
+  val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
 
   type tyco_syntax
   type simple_const_syntax
@@ -220,6 +221,11 @@
     else p
   end;
 
+fun applify opn cls fxy_ctxt p [] = p
+  | applify opn cls fxy_ctxt p ps =
+      (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
+        (p @@ enum "," opn cls ps);
+
 
 (* generic syntax *)