src/Pure/ML-Systems/ml_pretty.ML
changeset 61862 e2a9e46ac0fb
parent 38635 f76ad0771f67
child 61864 3a5992c3410c
     1.1 --- a/src/Pure/ML-Systems/ml_pretty.ML	Wed Dec 16 17:30:30 2015 +0100
     1.2 +++ b/src/Pure/ML-Systems/ml_pretty.ML	Thu Dec 17 17:32:01 2015 +0100
     1.3 @@ -10,11 +10,11 @@
     1.4  datatype pretty =
     1.5    Block of (string * string) * pretty list * int |
     1.6    String of string * int |
     1.7 -  Break of bool * int;
     1.8 +  Break of bool * int * int;
     1.9  
    1.10  fun block prts = Block (("", ""), prts, 2);
    1.11  fun str s = String (s, size s);
    1.12 -fun brk wd = Break (false, wd);
    1.13 +fun brk width = Break (false, width, 0);
    1.14  
    1.15  fun pair pretty1 pretty2 ((x, y), depth: int) =
    1.16    block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];