src/Tools/Code/code_printer.ML
changeset 39011 49b885736e8f
parent 38195 9728342bcd56
child 39137 caba168a3039
equal deleted inserted replaced
39010:a94559e26000 39011:49b885736e8f
    17   val @| : 'a list * 'a -> 'a list
    17   val @| : 'a list * 'a -> 'a list
    18   val str: string -> Pretty.T
    18   val str: string -> Pretty.T
    19   val concat: Pretty.T list -> Pretty.T
    19   val concat: Pretty.T list -> Pretty.T
    20   val brackets: Pretty.T list -> Pretty.T
    20   val brackets: Pretty.T list -> Pretty.T
    21   val enclose: string -> string -> Pretty.T list -> Pretty.T
    21   val enclose: string -> string -> Pretty.T list -> Pretty.T
       
    22   val commas: Pretty.T list -> Pretty.T list
    22   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
    23   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
    23   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    24   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    24   val semicolon: Pretty.T list -> Pretty.T
    25   val semicolon: Pretty.T list -> Pretty.T
    25   val doublesemicolon: Pretty.T list -> Pretty.T
    26   val doublesemicolon: Pretty.T list -> Pretty.T
    26   val indent: int -> Pretty.T -> Pretty.T
    27   val indent: int -> Pretty.T -> Pretty.T
   110 infixr 5 @|;
   111 infixr 5 @|;
   111 fun x @@ y = [x, y];
   112 fun x @@ y = [x, y];
   112 fun xs @| y = xs @ [y];
   113 fun xs @| y = xs @ [y];
   113 val str = Print_Mode.setmp [] Pretty.str;
   114 val str = Print_Mode.setmp [] Pretty.str;
   114 val concat = Pretty.block o Pretty.breaks;
   115 val concat = Pretty.block o Pretty.breaks;
       
   116 val commas = Print_Mode.setmp [] Pretty.commas;
   115 fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
   117 fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
   116 val brackets = enclose "(" ")" o Pretty.breaks;
   118 val brackets = enclose "(" ")" o Pretty.breaks;
   117 fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
   119 fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
   118 fun enum_default default sep l r [] = str default
   120 fun enum_default default sep l r [] = str default
   119   | enum_default default sep l r xs = enum sep l r xs;
   121   | enum_default default sep l r xs = enum sep l r xs;