src/Tools/Code/code_printer.ML
changeset 37638 82f9ce5a8274
parent 37449 034ebe92f090
child 37744 3daaf23b9ab4
     1.1 --- a/src/Tools/Code/code_printer.ML	Tue Jun 29 17:03:59 2010 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Wed Jun 30 11:38:51 2010 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4    val brackify: fixity -> Pretty.T list -> Pretty.T
     1.5    val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
     1.6    val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
     1.7 -  val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
     1.8 +  val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
     1.9  
    1.10    type tyco_syntax
    1.11    type simple_const_syntax
    1.12 @@ -230,10 +230,10 @@
    1.13      else p
    1.14    end;
    1.15  
    1.16 -fun applify opn cls fxy_ctxt p [] = p
    1.17 -  | applify opn cls fxy_ctxt p ps =
    1.18 +fun applify opn cls f fxy_ctxt p [] = p
    1.19 +  | applify opn cls f fxy_ctxt p ps =
    1.20        (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
    1.21 -        (p @@ enum "," opn cls ps);
    1.22 +        (p @@ enum "," opn cls (map f ps));
    1.23  
    1.24  
    1.25  (* generic syntax *)