--- 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 *)