src/Pure/ML-Systems/ml_pretty.ML
changeset 61864 3a5992c3410c
parent 61862 e2a9e46ac0fb
child 61869 ba466ac335e3
equal deleted inserted replaced
61863:931792ce2d83 61864:3a5992c3410c
     6 
     6 
     7 structure ML_Pretty =
     7 structure ML_Pretty =
     8 struct
     8 struct
     9 
     9 
    10 datatype pretty =
    10 datatype pretty =
    11   Block of (string * string) * pretty list * int |
    11   Block of (string * string) * pretty list * bool * int |
    12   String of string * int |
    12   String of string * int |
    13   Break of bool * int * int;
    13   Break of bool * int * int;
    14 
    14 
    15 fun block prts = Block (("", ""), prts, 2);
    15 fun block prts = Block (("", ""), prts, false, 2);
    16 fun str s = String (s, size s);
    16 fun str s = String (s, size s);
    17 fun brk width = Break (false, width, 0);
    17 fun brk width = Break (false, width, 0);
    18 
    18 
    19 fun pair pretty1 pretty2 ((x, y), depth: int) =
    19 fun pair pretty1 pretty2 ((x, y), depth: int) =
    20   block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
    20   block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];